diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
| commit | 056068abd228fefab4951a61700aa6d54fb88287 (patch) | |
| tree | 6bf44526caf535e464e33999641b39032901fa67 /cfrontend/Cshmgenproof.v | |
| parent | 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 (diff) | |
| download | compcert-kvx-056068abd228fefab4951a61700aa6d54fb88287.tar.gz compcert-kvx-056068abd228fefab4951a61700aa6d54fb88287.zip | |
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 42eae5da..74a6da5e 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -732,10 +732,10 @@ Lemma block_is_volatile_preserved: forall b, block_is_volatile tge b = block_is_volatile ge b. Proof. intros. unfold block_is_volatile. - destruct (Genv.find_var_info ge b) as []_eqn. + destruct (Genv.find_var_info ge b) eqn:?. exploit var_info_translated; eauto. intros [tv [A B]]. rewrite A. unfold transf_globvar in B. monadInv B. auto. - destruct (Genv.find_var_info tge b) as []_eqn. + destruct (Genv.find_var_info tge b) eqn:?. exploit var_info_rev_translated; eauto. intros [tv [A B]]. congruence. auto. Qed. @@ -761,7 +761,7 @@ Lemma match_env_globals: e!id = None -> te!id = None. Proof. - intros. destruct (te!id) as [[b sz] | ]_eqn; auto. + intros. destruct (te!id) as [[b sz] | ] eqn:?; auto. exploit me_local_inv; eauto. intros [ty EQ]. congruence. Qed. @@ -1284,7 +1284,7 @@ Proof. destruct H0. inv MK. econstructor; split. eapply plus_left. - destruct H0; subst ts'; constructor. + destruct H0; subst ts'. 2:constructor. constructor. apply star_one. constructor. traceEq. econstructor; eauto. constructor. econstructor; eauto. @@ -1355,7 +1355,7 @@ Proof. destruct H; subst x; monadInv TR; inv MTR; auto. destruct H0. inv MK. econstructor; split. - apply plus_one. destruct H0; subst ts'; constructor. + apply plus_one. destruct H0; subst ts'. 2:constructor. constructor. eapply match_states_skip; eauto. |