From b279716c76c387c6c5eec96388c0c35629858b4c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 26 Nov 2014 14:46:07 +0100 Subject: Introduce symbol environments (type Senv.t) as a restricted view on global environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events). --- 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 813944d6..18eab3b7 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1255,7 +1255,7 @@ Proof. inv H2. * (* true volatile access *) assert (V: vmatch bc v0 (Ifptr Glob)). - { inv H4; constructor. econstructor. eapply GE; eauto. } + { inv H4; simpl in *; constructor. econstructor. eapply GE; eauto. } destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. apply vnormalize_sound. eapply vmatch_ge; eauto. constructor. constructor. * (* normal memory access *) -- cgit