From e9fa9cbdc761f8c033e9b702f7485982faed3f7d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 30 Apr 2015 19:26:11 +0200 Subject: Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Val.lessdef, etc. --- backend/ValueDomain.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/ValueDomain.v') 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. -- cgit