diff options
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 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 *) |