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

1 files changed, 26 insertions, 26 deletions

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))