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/ValueDomain.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/ValueDomain.v')
| -rw-r--r-- | backend/ValueDomain.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index ff3ccfa1..b4c1df61 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3690,7 +3690,7 @@ Proof. Qed. Lemma vmatch_inj: - forall bc v x, vmatch bc v x -> val_inject (inj_of_bc bc) v v. + forall bc v x, vmatch bc v x -> Val.inject (inj_of_bc bc) v v. Proof. induction 1; econstructor. eapply pmatch_inj; eauto. rewrite Int.add_zero; auto. @@ -3698,7 +3698,7 @@ Proof. Qed. Lemma vmatch_list_inj: - forall bc vl xl, list_forall2 (vmatch bc) vl xl -> val_list_inject (inj_of_bc bc) vl vl. + forall bc vl xl, list_forall2 (vmatch bc) vl xl -> Val.inject_list (inj_of_bc bc) vl vl. Proof. induction 1; constructor. eapply vmatch_inj; eauto. auto. Qed. @@ -3761,7 +3761,7 @@ Proof. Qed. Lemma vmatch_inj_top: - forall bc v v', val_inject (inj_of_bc bc) v v' -> vmatch bc v Vtop. + forall bc v v', Val.inject (inj_of_bc bc) v v' -> vmatch bc v Vtop. Proof. intros. inv H; constructor. eapply pmatch_inj_top; eauto. Qed. |