diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-30 19:26:11 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-30 19:26:11 +0200 |
| commit | e9fa9cbdc761f8c033e9b702f7485982faed3f7d (patch) | |
| tree | 07eef17ccca466fd39d8d3ab0aab821ebfce177f /backend/ValueAnalysis.v | |
| parent | 7dd10e861c7ecbe74a781a6050ae1341bbe45dcd (diff) | |
| download | compcert-kvx-e9fa9cbdc761f8c033e9b702f7485982faed3f7d.tar.gz compcert-kvx-e9fa9cbdc761f8c033e9b702f7485982faed3f7d.zip | |
Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Val.lessdef, etc.
Diffstat (limited to 'backend/ValueAnalysis.v')
| -rw-r--r-- | backend/ValueAnalysis.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 8720ce50..28934ce9 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -923,7 +923,7 @@ Proof. rewrite JBELOW in H by auto. eapply inj_of_bc_inv; eauto. rewrite H; congruence. } - assert (VMTOP: forall v v', val_inject j' v v' -> vmatch bc' v Vtop). + assert (VMTOP: forall v v', Val.inject j' v v' -> vmatch bc' v Vtop). { intros. inv H; constructor. eapply PMTOP; eauto. } |