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 /driver/Compiler.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 'driver/Compiler.v')
| -rw-r--r-- | driver/Compiler.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index ed27f38..9db7f42 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -217,18 +217,18 @@ Proof. repeat rewrite compose_print_identity in H. simpl in H. set (p1 := Tailcall.transf_program p) in *. - destruct (Inlining.transf_program p1) as [p11|]_eqn; simpl in H; try discriminate. + destruct (Inlining.transf_program p1) as [p11|] eqn:?; simpl in H; try discriminate. set (p12 := Renumber.transf_program p11) in *. set (p2 := Constprop.transf_program p12) in *. set (p21 := Renumber.transf_program p2) in *. - destruct (CSE.transf_program p21) as [p3|]_eqn; simpl in H; try discriminate. - destruct (Allocation.transf_program p3) as [p4|]_eqn; simpl in H; try discriminate. + destruct (CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate. + destruct (Allocation.transf_program p3) as [p4|] eqn:?; simpl in H; try discriminate. set (p5 := Tunneling.tunnel_program p4) in *. - destruct (Linearize.transf_program p5) as [p6|]_eqn; simpl in H; try discriminate. + destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate. set (p7 := CleanupLabels.transf_program p6) in *. set (p8 := Reload.transf_program p7) in *. set (p9 := RRE.transf_program p8) in *. - destruct (Stacking.transf_program p9) as [p10|]_eqn; simpl in H; try discriminate. + destruct (Stacking.transf_program p9) as [p10|] eqn:?; simpl in H; try discriminate. assert(TY1: LTLtyping.wt_program p5). eapply Tunnelingtyping.program_typing_preserved. @@ -274,7 +274,7 @@ Proof. repeat rewrite compose_print_identity in H. simpl in H. set (p1 := Selection.sel_program p) in *. - destruct (RTLgen.transl_program p1) as [p2|]_eqn; simpl in H; try discriminate. + destruct (RTLgen.transl_program p1) as [p2|] eqn:?; simpl in H; try discriminate. eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption. exact (fst (transf_rtl_program_correct _ _ H)). |