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 /common/AST.v | |
| parent | 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 (diff) | |
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 'common/AST.v')
| -rw-r--r-- | common/AST.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/common/AST.v b/common/AST.v index 40da732..d2065d6 100644 --- a/common/AST.v +++ b/common/AST.v @@ -225,10 +225,10 @@ Proof. revert x EQ H0. induction (prog_defs p); simpl; intros. inv EQ. contradiction. destruct a as [id [f|v]]. - destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ. + destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. exists f; auto. exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. - destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ. + destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. Qed. @@ -245,10 +245,10 @@ Proof. revert x EQ H0. induction (prog_defs p); simpl; intros. inv EQ. contradiction. destruct a as [id [f|v]]. - destruct (transf_fun f) as [tf1|msg]_eqn; monadInv EQ. + destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. - destruct (transf_globvar v) as [tv1|msg]_eqn; monadInv EQ. + destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto. exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. @@ -394,11 +394,11 @@ Proof. monadInv EQ. constructor. destruct a as [id [f|v]]. (* function *) - destruct (transf_fun f) as [tf|?]_eqn; monadInv EQ. + destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ. constructor; auto. constructor; auto. (* variable *) unfold transf_globvar in EQ. - destruct (transf_var (gvar_info v)) as [tinfo|?]_eqn; simpl in EQ; monadInv EQ. + destruct (transf_var (gvar_info v)) as [tinfo|?] eqn:?; simpl in EQ; monadInv EQ. constructor; auto. destruct v; simpl in *. constructor; auto. Qed. |