From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: 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 --- cfrontend/Cshmgenproof.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 42eae5d..74a6da5 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. -- cgit v1.2.3