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/ValueAnalysis.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/ValueAnalysis.v') 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. } -- cgit