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/SimplLocalsproof.v | 52 ++++++++++++++++++++++---------------------- 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'cfrontend/SimplLocalsproof.v') diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index f58a2130..8df7b6ea 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -83,7 +83,7 @@ Lemma type_of_global_preserved: Proof. unfold type_of_global; intros. rewrite varinfo_preserved. destruct (Genv.find_var_info ge id). auto. - destruct (Genv.find_funct_ptr ge id) as [fd|]_eqn; inv H. + destruct (Genv.find_funct_ptr ge id) as [fd|] eqn:?; inv H. exploit function_ptr_translated; eauto. intros [tf [A B]]. rewrite A. decEq. apply type_of_fundef_preserved; auto. Qed. @@ -183,12 +183,12 @@ Lemma match_envs_extcall: Proof. intros. eapply match_envs_invariant; eauto. intros. destruct H0. eapply H8. intros; red. auto. auto. - red in H2. intros. destruct (f b) as [[b' delta]|]_eqn. + red in H2. intros. destruct (f b) as [[b' delta]|] eqn:?. eapply H1; eauto. - destruct (f' b) as [[b' delta]|]_eqn; auto. + destruct (f' b) as [[b' delta]|] eqn:?; auto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. - intros. destruct (f b) as [[b'' delta']|]_eqn. eauto. + intros. destruct (f b) as [[b'' delta']|] eqn:?. eauto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. Qed. @@ -405,7 +405,7 @@ Lemma match_envs_set_temp: match_envs f cenv e (PTree.set id v le) m lo hi te (PTree.set id tv tle) tlo thi. Proof. intros. unfold check_temp in H1. - destruct (VSet.mem id cenv) as []_eqn; monadInv H1. + destruct (VSet.mem id cenv) eqn:?; monadInv H1. destruct H. constructor; eauto; intros. (* vars *) generalize (me_vars0 id0); intros MV; inv MV. @@ -477,8 +477,8 @@ Remark add_local_variable_charact: VSet.In id1 cenv \/ exists chunk, access_mode ty = By_value chunk /\ id = id1 /\ VSet.mem id atk = false. Proof. intros. unfold add_local_variable. split; intros. - destruct (access_mode ty) as []_eqn; auto. - destruct (VSet.mem id atk) as []_eqn; auto. + destruct (access_mode ty) eqn:?; auto. + destruct (VSet.mem id atk) eqn:?; auto. rewrite VSF.add_iff in H. destruct H; auto. right; exists m; auto. destruct H as [A | [chunk [A [B C]]]]. destruct (access_mode ty); auto. destruct (VSet.mem id atk); auto. rewrite VSF.add_iff; auto. @@ -639,7 +639,7 @@ Proof. (* inductive case *) simpl in H1. inv H1. simpl. - destruct (VSet.mem id cenv) as []_eqn. simpl. + destruct (VSet.mem id cenv) eqn:?. simpl. (* variable is lifted out of memory *) exploit Mem.alloc_left_unmapped_inject; eauto. intros [j1 [A [B [C D]]]]. @@ -782,7 +782,7 @@ Proof. assert (forall id l1 l2, (In id (var_names l1) -> In id (var_names l2)) -> (create_undef_temps l1)!id = None \/ (create_undef_temps l1)!id = (create_undef_temps l2)!id). - intros. destruct ((create_undef_temps l1)!id) as [v1|]_eqn; auto. + intros. destruct ((create_undef_temps l1)!id) as [v1|] eqn:?; auto. exploit create_undef_temps_inv; eauto. intros [A B]. subst v1. exploit list_in_map_inv. unfold var_names in H. apply H. eexact B. intros [[id1 ty1] [P Q]]. simpl in P; subst id1. @@ -813,7 +813,7 @@ Remark filter_charact: In x (List.filter f l) <-> In x l /\ f x = true. Proof. induction l; simpl. tauto. - destruct (f a) as []_eqn. + destruct (f a) eqn:?. simpl. rewrite IHl. intuition congruence. intuition congruence. Qed. @@ -902,7 +902,7 @@ Proof. unfold var_names in i. exploit list_in_map_inv; eauto. intros [[id' ty] [EQ IN]]; simpl in EQ; subst id'. exploit F; eauto. intros [b [P R]]. - destruct (VSet.mem id cenv) as []_eqn. + destruct (VSet.mem id cenv) eqn:?. (* local var, lifted *) destruct R as [U V]. exploit H2; eauto. intros [chunk X]. eapply match_var_lifted with (v := Vundef) (tv := Vundef); eauto. @@ -918,7 +918,7 @@ Proof. (* non-local var *) exploit G; eauto. unfold empty_env. rewrite PTree.gempty. intros [U V]. eapply match_var_not_local; eauto. - destruct (VSet.mem id cenv) as []_eqn; auto. + destruct (VSet.mem id cenv) eqn:?; auto. elim n; eauto. (* temps *) @@ -1072,7 +1072,7 @@ Proof. (* inductive case *) inv NOREPET. inv CASTED. inv VINJ. exploit me_vars; eauto. instantiate (1 := id); intros MV. - destruct (VSet.mem id cenv) as []_eqn. + destruct (VSet.mem id cenv) eqn:?. (* lifted to temp *) eapply IHbind_parameters with (tle1 := PTree.set id v' tle1); eauto. eapply match_envs_assign_lifted; eauto. @@ -1164,7 +1164,7 @@ Proof. induction l; simpl; intros. contradiction. destruct a as [[b1 lo1] hi1]. - destruct (Mem.free m b1 lo1 hi1) as [m1|]_eqn; try discriminate. + destruct (Mem.free m b1 lo1 hi1) as [m1|] eqn:?; try discriminate. destruct H0. inv H0. eapply Mem.free_range_perm; eauto. red; intros. eapply Mem.perm_free_3; eauto. eapply IHl; eauto. Qed. @@ -1209,7 +1209,7 @@ Lemma free_list_right_inject: Proof. induction l; simpl; intros. congruence. - destruct a as [[b lo] hi]. destruct (Mem.free m2 b lo hi) as [m21|]_eqn; try discriminate. + destruct a as [[b lo] hi]. destruct (Mem.free m2 b lo hi) as [m21|] eqn:?; try discriminate. eapply IHl with (m2 := m21); eauto. eapply Mem.free_right_inject; eauto. Qed. @@ -1380,8 +1380,8 @@ Proof. destruct (classify_cmp ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. destruct (Int.eq i Int.zero); try discriminate; auto. destruct (Int.eq i Int.zero); try discriminate; auto. - destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) as []_eqn; try discriminate. - destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) as []_eqn; try discriminate. + destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate. + destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate. simpl in H3. rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb). rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0). @@ -1509,7 +1509,7 @@ Proof. (* addrof *) exploit eval_simpl_lvalue; eauto. destruct a; auto with compat. - destruct a; auto. destruct (VSet.mem i cenv) as []_eqn; auto. + destruct a; auto. destruct (VSet.mem i cenv) eqn:?; auto. elim (H0 i). apply VSet.singleton_2. auto. apply VSet.mem_2. auto. intros [b' [ofs' [A B]]]. exists (Vptr b' ofs'); split; auto. constructor; auto. @@ -1529,7 +1529,7 @@ Proof. (* rval *) assert (EITHER: (exists id, exists ty, a = Evar id ty /\ VSet.mem id cenv = true) \/ (match a with Evar id _ => VSet.mem id cenv = false | _ => True end)). - destruct a; auto. destruct (VSet.mem i cenv) as []_eqn; auto. left; exists i; exists t; auto. + destruct a; auto. destruct (VSet.mem i cenv) eqn:?; auto. left; exists i; exists t; auto. destruct EITHER as [ [id [ty [EQ OPT]]] | NONOPT ]. (* a variable pulled out of memory *) subst a. simpl. rewrite OPT. @@ -1696,10 +1696,10 @@ Lemma match_cont_extcall: Proof. intros. eapply match_cont_invariant; eauto. destruct H0. intros. eapply H5; eauto. - red in H2. intros. destruct (f b) as [[b' delta] | ]_eqn. auto. - destruct (f' b) as [[b' delta] | ]_eqn; auto. + red in H2. intros. destruct (f b) as [[b' delta] | ] eqn:?. auto. + destruct (f' b) as [[b' delta] | ] eqn:?; auto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. - red in H2. intros. destruct (f b) as [[b'' delta''] | ]_eqn. auto. + red in H2. intros. destruct (f b) as [[b'' delta''] | ] eqn:?. auto. exploit H2; eauto. unfold Mem.valid_block. intros [A B]. omegaContradiction. Qed. @@ -1752,7 +1752,7 @@ Remark free_list_nextblock: Proof. induction l; simpl; intros. congruence. - destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|]_eqn; try discriminate. + destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate. transitivity (Mem.nextblock m1). eauto. eapply Mem.nextblock_free; eauto. Qed. @@ -1764,7 +1764,7 @@ Remark free_list_load: Proof. induction l; simpl; intros. inv H; auto. - destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|]_eqn; try discriminate. + destruct a. destruct p. destruct (Mem.free m b z0 z) as [m1|] eqn:?; try discriminate. transitivity (Mem.load chunk m1 b' 0). eauto. eapply Mem.load_free. eauto. left. assert (b' < b) by eauto. unfold block; omega. Qed. @@ -1860,7 +1860,7 @@ Remark is_liftable_var_charact: end. Proof. intros. destruct a; simpl; auto. - destruct (VSet.mem i cenv) as []_eqn. + destruct (VSet.mem i cenv) eqn:?. exists t; auto. auto. Qed. @@ -2202,7 +2202,7 @@ Proof. apply val_list_inject_incr with j'; eauto. eexact B. eexact C. intros. apply (create_undef_temps_lifted id f). auto. - intros. destruct (create_undef_temps (fn_temps f))!id as [v|]_eqn; auto. + intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto. exploit create_undef_temps_inv; eauto. intros [P Q]. elim (H3 id id); auto. intros [tel [tm1 [P [Q [R [S T]]]]]]. change (cenv_for_gen (addr_taken_stmt (fn_body f)) (fn_params f ++ fn_vars f)) -- cgit