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 --- backend/Inliningproof.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'backend/Inliningproof.v') diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 8de84875..9536141a 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -306,7 +306,7 @@ Lemma range_private_free_left: range_private F m1 m' sp base hi. Proof. intros; red; intros. - destruct (zlt ofs (base + Zmax sz 0)). + destruct (zlt ofs (base + Zmax sz 0)) as [z|z]. red; split. replace ofs with ((ofs - base) + base) by omega. eapply Mem.perm_inject; eauto. @@ -342,7 +342,7 @@ Proof. red; intros. exploit RP; eauto. intros [A B]. destruct UNCH as [U1 U2]. split. auto. - intros. red in SEP. destruct (F b) as [[sp1 delta1] |]_eqn. + intros. red in SEP. destruct (F b) as [[sp1 delta1] |] eqn:?. exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. red; intros; eelim B; eauto. eapply PERM; eauto. red. destruct (zlt b (Mem.nextblock m1)); auto. @@ -710,7 +710,7 @@ Proof. induction 1; intros. apply match_stacks_nil with bound1; auto. inv MG. constructor; intros; eauto. - destruct (F1 b1) as [[b2' delta']|]_eqn. + destruct (F1 b1) as [[b2' delta']|] eqn:?. exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto. exploit SEP; eauto. intros [A B]. elim B. red. omega. eapply match_stacks_cons; eauto. @@ -919,7 +919,7 @@ Proof. eapply agree_val_regs; eauto. (* inlined *) assert (fd = Internal f0). - simpl in H0. destruct (Genv.find_symbol ge id) as [b|]_eqn; try discriminate. + simpl in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:?; try discriminate. exploit (funenv_program_compat prog); eauto. intros. unfold ge in H0. congruence. subst fd. @@ -973,7 +973,7 @@ Proof. eapply Mem.free_left_inject; eauto. (* inlined *) assert (fd = Internal f0). - simpl in H0. destruct (Genv.find_symbol ge id) as [b|]_eqn; try discriminate. + simpl in H0. destruct (Genv.find_symbol ge id) as [b|] eqn:?; try discriminate. exploit (funenv_program_compat prog); eauto. intros. unfold ge in H0. congruence. subst fd. -- cgit