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

6 files changed, 58 insertions, 56 deletions

diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index 3d0c57f5..d618d44d 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -1122,7 +1122,8 @@ Proof.
   intros. simpl in H2.
   destruct (transl_cond_correct tge tf cond args _ _ rs m' H2)
   as [rs' [A [B C]]]. 
-  unfold PregEq.t in B; rewrite EC in B.
+  rewrite EC in B (* 8.4 *)
+   || (unfold PregEq.t in B; rewrite EC in B) (* 8.3 *).
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   exists (Pjcc c1 lbl); exists k; exists rs'.
@@ -1130,8 +1131,8 @@ Proof.
   split. eapply agree_exten_temps; eauto. 
   simpl. rewrite B. auto.
 (* jcc; jcc *)
-  destruct (eval_testcond c1 rs') as [b1|]_eqn;
-  destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
   destruct b1.   
   (* first jcc jumps *)
   exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'.
@@ -1147,8 +1148,8 @@ Proof.
   simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0.
   destruct b2; auto || discriminate.
 (* jcc2 *)
-  destruct (eval_testcond c1 rs') as [b1|]_eqn;
-  destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
   destruct (andb_prop _ _ H4). subst. 
   exists (Pjcc2 c1 c2 lbl); exists k; exists rs'.
   split. eexact A.
@@ -1169,7 +1170,8 @@ Proof.
   left; eapply exec_straight_steps; eauto. intros. simpl in H0. 
   destruct (transl_cond_correct tge tf cond args _ _ rs m' H0)
   as [rs' [A [B C]]]. 
-  unfold PregEq.t in B; rewrite EC in B.
+  rewrite EC in B (* 8.4 *)
+   || (unfold PregEq.t in B; rewrite EC in B) (* 8.3 *).
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   econstructor; split.
@@ -1178,8 +1180,8 @@ Proof.
   split. apply agree_nextinstr. eapply agree_exten_temps; eauto.
   simpl; congruence.
 (* jcc ; jcc *)
-  destruct (eval_testcond c1 rs') as [b1|]_eqn;
-  destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
   destruct (orb_false_elim _ _ H2); subst.
   econstructor; split.
   eapply exec_straight_trans. eexact A. 
@@ -1188,8 +1190,8 @@ Proof.
   split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten_temps; eauto.
   simpl; congruence.
 (* jcc2 *)
-  destruct (eval_testcond c1 rs') as [b1|]_eqn;
-  destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
   exists (nextinstr rs'); split.
   eapply exec_straight_trans. eexact A. 
   apply exec_straight_one. simpl. 
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 0a466773..7a4348b3 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -1099,12 +1099,12 @@ Proof.
   rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
   destruct (Int.ltu i i0); reflexivity.
 (* int ptr *)
-  destruct (Int.eq i Int.zero) as []_eqn; try discriminate.
+  destruct (Int.eq i Int.zero) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
   rewrite Heqb1; reflexivity. 
   rewrite Heqb1; reflexivity.
 (* ptr int *)
-  destruct (Int.eq i0 Int.zero) as []_eqn; try discriminate.
+  destruct (Int.eq i0 Int.zero) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
   rewrite Heqb1; reflexivity. 
   rewrite Heqb1; reflexivity.
@@ -1396,13 +1396,13 @@ Proof.
 (* comp *)
   simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) as []_eqn; auto.
+  split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:?; auto.
   eapply testcond_for_signed_comparison_correct; eauto. 
   intros. unfold compare_ints. repeat SOther.
 (* compu *)
   simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) as []_eqn; auto.
+  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto.
   eapply testcond_for_unsigned_comparison_correct; eauto. 
   intros. unfold compare_ints. repeat SOther.
 (* compimm *)
@@ -1412,13 +1412,13 @@ Proof.
   eapply testcond_for_signed_comparison_correct; eauto. 
   intros. unfold compare_ints. repeat SOther.
   econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
-  split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) as []_eqn; auto.
+  split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:?; auto.
   eapply testcond_for_signed_comparison_correct; eauto. 
   intros. unfold compare_ints. repeat SOther.
 (* compuimm *)
   simpl. rewrite (ireg_of_eq _ _ EQ).
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) as []_eqn; auto.
+  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:?; auto.
   eapply testcond_for_unsigned_comparison_correct; eauto. 
   intros. unfold compare_ints. repeat SOther.
 (* compf *)
@@ -1613,22 +1613,22 @@ Proof.
 (* div *)
   apply SAME.
   specialize (divs_mods_exist (rs x0) (rs x1)). rewrite H0. 
-  destruct (Val.mods (rs x0) (rs x1)) as [vr|]_eqn; intros; try contradiction.
+  destruct (Val.mods (rs x0) (rs x1)) as [vr|] eqn:?; intros; try contradiction.
   eapply mk_div_correct with (dsem := Val.divs) (msem := Val.mods); eauto.
 (* divu *)
   apply SAME.
   specialize (divu_modu_exist (rs x0) (rs x1)). rewrite H0. 
-  destruct (Val.modu (rs x0) (rs x1)) as [vr|]_eqn; intros; try contradiction.
+  destruct (Val.modu (rs x0) (rs x1)) as [vr|] eqn:?; intros; try contradiction.
   eapply mk_div_correct with (dsem := Val.divu) (msem := Val.modu); eauto.
 (* mod *)
   apply SAME.
   specialize (divs_mods_exist (rs x0) (rs x1)). rewrite H0. 
-  destruct (Val.divs (rs x0) (rs x1)) as [vq|]_eqn; intros; try contradiction.
+  destruct (Val.divs (rs x0) (rs x1)) as [vq|] eqn:?; intros; try contradiction.
   eapply mk_mod_correct with (dsem := Val.divs) (msem := Val.mods); eauto.
 (* modu *)
   apply SAME.
   specialize (divu_modu_exist (rs x0) (rs x1)). rewrite H0. 
-  destruct (Val.divu (rs x0) (rs x1)) as [vq|]_eqn; intros; try contradiction.
+  destruct (Val.divu (rs x0) (rs x1)) as [vq|] eqn:?; intros; try contradiction.
   eapply mk_mod_correct with (dsem := Val.divu) (msem := Val.modu); eauto.
 (* shl *)
   apply SAME. eapply mk_shift_correct; eauto. 
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 1a0508cd..90037435 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -158,10 +158,10 @@ Proof.
   destruct (Int.ltu n Int.iwordsize); simpl; auto.
   eapply eval_static_addressing_correct; eauto.
   unfold eval_static_intoffloat.
-  destruct (Float.intoffloat n1) as []_eqn; simpl in H0; inv H0.
+  destruct (Float.intoffloat n1) eqn:?; simpl in H0; inv H0.
   simpl; auto.
   destruct (propagate_float_constants tt); simpl; auto.
-  unfold eval_static_condition_val. destruct (eval_static_condition c vl0) as [b|]_eqn.
+  unfold eval_static_condition_val. destruct (eval_static_condition c vl0) as [b|] eqn:?.
   rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). 
   destruct b; simpl; auto.
   simpl; auto.
@@ -290,7 +290,7 @@ Proof.
   exists (Vint Int.zero); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_one; auto.
-  destruct (Int.is_power2 n) as []_eqn; intros.
+  destruct (Int.is_power2 n) eqn:?; intros.
   rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). apply make_shlimm_correct; auto. 
   econstructor; split; eauto. auto. 
 Qed.
@@ -303,8 +303,8 @@ Lemma make_divimm_correct:
   exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
-  destruct (Int.is_power2 n) as []_eqn.
-  destruct (Int.ltu i (Int.repr 31)) as []_eqn.
+  destruct (Int.is_power2 n) eqn:?.
+  destruct (Int.ltu i (Int.repr 31)) eqn:?.
   exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. 
   exists v; auto.
   exists v; auto.
@@ -318,7 +318,7 @@ Lemma make_divuimm_correct:
   exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
-  destruct (Int.is_power2 n) as []_eqn.
+  destruct (Int.is_power2 n) eqn:?.
   replace v with (Val.shru rs#r1 (Vint i)). 
   eapply make_shruimm_correct; eauto.
   eapply Val.divu_pow2; eauto. congruence.
@@ -333,7 +333,7 @@ Lemma make_moduimm_correct:
   exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_moduimm.
-  destruct (Int.is_power2 n) as []_eqn.
+  destruct (Int.is_power2 n) eqn:?.
   exists v; split; auto. simpl. decEq. eapply Val.modu_pow2; eauto. congruence.
   exists v; auto.
 Qed.
@@ -430,10 +430,10 @@ Lemma builtin_strength_reduction_correct:
 Proof.
   intros until m'. unfold builtin_strength_reduction.
   destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA.
-  unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|]_eqn; rewrite H in H0.
+  unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H in H0.
   rewrite volatile_load_global_charact. exists b; auto. 
   inv H0.
-  unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|]_eqn; rewrite H1 in H0.
+  unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H1 in H0.
   rewrite volatile_store_global_charact. exists b; auto. 
   inv H0.
   auto.
diff --git a/ia32/Op.v b/ia32/Op.v
index 81695945..93a867a2 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -642,8 +642,8 @@ Proof.
   right. apply Int.no_overlap_sound; auto. 
 (* Aglobal *)
   unfold symbol_address in *. 
-  destruct (Genv.find_symbol ge i1) as []_eqn; inv H2.
-  destruct (Genv.find_symbol ge i) as []_eqn; inv H1.
+  destruct (Genv.find_symbol ge i1) eqn:?; inv H2.
+  destruct (Genv.find_symbol ge i) eqn:?; inv H1.
   destruct (ident_eq i i1). subst.
   replace (Int.unsigned n1) with (Int.unsigned (Int.add Int.zero n1)).
   replace (Int.unsigned n2) with (Int.unsigned (Int.add Int.zero n2)).
@@ -653,9 +653,9 @@ Proof.
   left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto.
 (* Abased *)
   unfold symbol_address in *. 
-  destruct (Genv.find_symbol ge i1) as []_eqn; simpl in *; try discriminate.
+  destruct (Genv.find_symbol ge i1) eqn:?; simpl in *; try discriminate.
   destruct v; inv H2.
-  destruct (Genv.find_symbol ge i) as []_eqn; inv H1.
+  destruct (Genv.find_symbol ge i) eqn:?; inv H1.
   destruct (ident_eq i i1). subst.
   rewrite (Int.add_commut i0 i3). rewrite (Int.add_commut i2 i3).
   right. apply Int.no_overlap_sound; auto. 
@@ -776,8 +776,8 @@ Opaque Int.add.
     Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
     Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
   intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-  destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) as []_eqn; try discriminate.
-  destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) as []_eqn; try discriminate.
+  destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
+  destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
   rewrite (valid_pointer_inj _ H2 Heqb4).
   rewrite (valid_pointer_inj _ H Heqb0). simpl.
   destruct (zeq b1 b0); simpl in H1.
@@ -878,7 +878,7 @@ Proof.
   inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2.
   exists (Vint i); auto.
   inv H4; simpl in H1; inv H1. simpl. TrivialExists.
-  subst v1. destruct (eval_condition c vl1 m1) as []_eqn.
+  subst v1. destruct (eval_condition c vl1 m1) eqn:?.
   exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
   destruct b; simpl; constructor.
   simpl; constructor.
@@ -995,7 +995,7 @@ Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 Remark symbol_address_inject:
   forall id ofs, val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs).
 Proof.
-  intros. unfold symbol_address. destruct (Genv.find_symbol genv id) as []_eqn; auto.
+  intros. unfold symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
   exploit (proj1 globals); eauto. intros. 
   econstructor; eauto. rewrite Int.add_zero; auto.
 Qed.
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index da08de8d..601869b8 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -787,7 +787,7 @@ let print_init oc = function
 	(camlint64_of_coqint (Floats.Float.bits_of_double n))
 	comment (camlfloat_of_coqfloat n)
   | Init_space n ->
-      let n = camlint_of_z n in
+      let n = Z.to_int32 n in
       if n > 0l then fprintf oc "	.space	%ld\n" n
   | Init_addrof(symb, ofs) ->
       fprintf oc "	.long	%a\n" 
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 136a7652..18deca64 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -228,12 +228,12 @@ Proof.
   destruct (shlimm_match a); intros; InvEval.
   exists (Vint (Int.shl n1 n)); split. EvalOp. 
   simpl. destruct (Int.ltu n Int.iwordsize); auto.
-  destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn.
+  destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp.
   subst. destruct v1; simpl; auto. 
   rewrite Heqb.
-  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl; auto.
+  destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
+  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl; auto.
   rewrite Int.add_commut. rewrite Int.shl_shl; auto. rewrite Int.add_commut; auto.
   subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. 
   simpl. auto.
@@ -259,12 +259,12 @@ Proof.
   destruct (shruimm_match a); intros; InvEval.
   exists (Vint (Int.shru n1 n)); split. EvalOp. 
   simpl. destruct (Int.ltu n Int.iwordsize); auto.
-  destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn.
+  destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp.
   subst. destruct v1; simpl; auto. 
   rewrite Heqb.
-  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl; auto.
+  destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
+  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl; auto.
   rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto.
   subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. 
   simpl. auto.
@@ -281,12 +281,12 @@ Proof.
   destruct (shrimm_match a); intros; InvEval.
   exists (Vint (Int.shr n1 n)); split. EvalOp. 
   simpl. destruct (Int.ltu n Int.iwordsize); auto.
-  destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn.
+  destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp.
   subst. destruct v1; simpl; auto. 
   rewrite Heqb.
-  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl; auto.
+  destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
+  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl; auto.
   rewrite Int.add_commut. rewrite Int.shr_shr; auto. rewrite Int.add_commut; auto.
   subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. 
   simpl. auto.
@@ -417,25 +417,25 @@ Proof.
   InvEval. rewrite Val.or_commut. apply eval_orimm; auto. 
   InvEval. apply eval_orimm; auto.
 (* shlimm - shruimm *)
-  destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) as []_eqn.
+  destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
   destruct (andb_prop _ _ Heqb0). 
   generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ.
   InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. 
   exists (Val.ror v0 (Vint n2)); split. EvalOp.
   destruct v0; simpl; auto. 
-  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto.
-  destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto.
+  destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
+  destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
   simpl. rewrite <- Int.or_ror; auto.
   TrivialExists. 
 (* shruimm - shlimm *) 
-  destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) as []_eqn.
+  destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
   destruct (andb_prop _ _ Heqb0). 
   generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ.
   InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. 
   exists (Val.ror v1 (Vint n2)); split. EvalOp.
   destruct v1; simpl; auto. 
-  destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto.
-  destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto.
+  destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
+  destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
   simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto.
   TrivialExists. 
 (* default *)
@@ -717,7 +717,7 @@ Theorem eval_intuoffloat:
   exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros. destruct x; simpl in H0; try discriminate.
-  destruct (Float.intuoffloat f) as [n|]_eqn; simpl in H0; inv H0.
+  destruct (Float.intuoffloat f) as [n|] eqn:?; simpl in H0; inv H0.
   exists (Vint n); split; auto. unfold intuoffloat.
   set (im := Int.repr Int.half_modulus).
   set (fm := Float.floatofintu im).
@@ -729,7 +729,7 @@ Proof.
   econstructor. instantiate (1 := Vfloat fm). EvalOp. 
   eapply eval_Econdition with (vb := Float.cmp Clt f fm).
   eauto with evalexpr. auto.
-  destruct (Float.cmp Clt f fm) as []_eqn.
+  destruct (Float.cmp Clt f fm) eqn:?.
   exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ.
   EvalOp. simpl. rewrite EQ; auto.
   exploit Float.intuoffloat_intoffloat_2; eauto. 
@@ -763,7 +763,7 @@ Proof.
   eapply eval_Econdition with (vb := Int.ltu i Float.ox8000_0000).
   constructor. eauto. constructor.
   simpl. auto.
-  destruct (Int.ltu i Float.ox8000_0000) as []_eqn.
+  destruct (Int.ltu i Float.ox8000_0000) eqn:?.
   rewrite Float.floatofintu_floatofint_1; auto.
   unfold floatofint. EvalOp. 
   exploit (eval_addimm (Int.neg Float.ox8000_0000) (Vint i :: le) (Eletvar 0)); eauto.