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

5 files changed, 33 insertions, 31 deletions

diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 2af4f70..f1c206e 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1516,6 +1516,7 @@ Lemma transl_load_correct:
 Proof.
   intros.
   exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
+  unfold PregEq.t.
   intros [a' [A B]]. 
   exploit Mem.loadv_extends; eauto. intros [v' [C D]].
   apply transl_load_store_correct with ms; auto.
@@ -1570,6 +1571,7 @@ Lemma transl_store_correct:
 Proof.
   intros.
   exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
+  unfold PregEq.t.
   intros [a' [A B]].
   assert (Z: Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto.
   exploit Mem.storev_extends; eauto. intros [m1' [C D]].
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index eef3944..7d557c6 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -155,7 +155,7 @@ Proof.
   destruct (propagate_float_constants tt); simpl; auto.
 
   unfold eval_static_condition_val, Val.of_optbool.
-  destruct (eval_static_condition c vl0) as []_eqn.
+  destruct (eval_static_condition c vl0) eqn:?.
   rewrite (eval_static_condition_correct _ _ _ m _ H Heqo).
   destruct b; simpl; auto. 
   simpl; auto.
@@ -240,7 +240,7 @@ Proof.
   intros; unfold make_shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shl_zero. auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn; intros.
+  destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
   rewrite Val.shl_rolm; auto. econstructor; split; eauto. auto. 
   econstructor; split; eauto. simpl. congruence.
 Qed.
@@ -254,7 +254,7 @@ Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shr_zero. auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn.
+  destruct (Int.ltu n Int.iwordsize) eqn:?.
   econstructor; split; eauto. simpl. auto.
   econstructor; split; eauto. simpl. congruence.
 Qed.
@@ -268,7 +268,7 @@ Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
   exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn; intros.
+  destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
   rewrite Val.shru_rolm; auto. econstructor; split; eauto. auto. 
   econstructor; split; eauto. simpl. congruence.
 Qed.
@@ -284,7 +284,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). rewrite Val.shl_rolm. 
   econstructor; split; eauto. auto. 
   eapply Int.is_power2_range; eauto.
@@ -299,8 +299,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.
@@ -314,7 +314,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:?. 
   econstructor; split. simpl; eauto.
   exploit Int.is_power2_range; eauto. intros RANGE.
   rewrite <- Val.shru_rolm; auto. rewrite H0 in H. 
@@ -439,10 +439,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/powerpc/Op.v b/powerpc/Op.v
index e59e15f..58bcb2c 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -576,8 +576,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)).
@@ -587,9 +587,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. 
@@ -706,8 +706,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.
@@ -792,7 +792,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; inv H2; simpl; auto.
-  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.
@@ -923,7 +923,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/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index a20448c..f56c3f2 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -924,7 +924,7 @@ let print_init oc = function
                  (Int64.logand b 0xFFFFFFFFL)
                  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/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 5e49366..7be8858 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -232,7 +232,7 @@ Proof.
   red; intros.  unfold shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn. 
+  destruct (Int.ltu n Int.iwordsize) eqn:?. 
   rewrite Val.shl_rolm; auto. apply eval_rolm; auto. 
   TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
@@ -244,7 +244,7 @@ Proof.
   red; intros.  unfold shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn. 
+  destruct (Int.ltu n Int.iwordsize) eqn:?. 
   rewrite Val.shru_rolm; auto. apply eval_rolm; auto. 
   TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
 Qed.
@@ -257,7 +257,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
   case (shrimm_match a); intros.
-  destruct (Int.lt mask1 Int.zero) as []_eqn. 
+  destruct (Int.lt mask1 Int.zero) eqn:?. 
   TrivialExists.
   replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)). 
   apply eval_shruimm; auto.
@@ -331,7 +331,7 @@ Proof.
   InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
   set (n' := Int.and n n2). 
   destruct (Int.eq (Int.shru (Int.shl n' amount) amount) n' &&
-            Int.ltu amount Int.iwordsize) as []_eqn.
+            Int.ltu amount Int.iwordsize) eqn:?.
   InvEval. destruct (andb_prop _ _ Heqb). 
   generalize (Int.eq_spec (Int.shru (Int.shl n' amount) amount) n'). rewrite H1; intros.
   replace (Val.and x (Vint n))
@@ -349,7 +349,7 @@ Proof.
   destruct v1; auto. simpl. unfold Int.rolm. rewrite Int.and_assoc. 
   decEq. decEq. decEq. apply Int.and_commut.
   destruct (Int.eq (Int.shru (Int.shl n amount) amount) n &&
-            Int.ltu amount Int.iwordsize) as []_eqn.
+            Int.ltu amount Int.iwordsize) eqn:?.
   InvEval. destruct (andb_prop _ _ Heqb). 
   generalize (Int.eq_spec (Int.shru (Int.shl n amount) amount) n). rewrite H0; intros.
   replace (Val.and x (Vint n))
@@ -402,20 +402,20 @@ Theorem eval_or: binary_constructor_sound or Val.or.
 Proof.
   red; intros until y; unfold or; case (or_match a b); intros.
 (* rolm - rolm *)
-  destruct (Int.eq amount1 amount2 && same_expr_pure t1 t2) as []_eqn.
+  destruct (Int.eq amount1 amount2 && same_expr_pure t1 t2) eqn:?.
   destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec amount1 amount2). rewrite H1. intro. subst amount2.
   InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. 
   rewrite Val.or_rolm. TrivialExists.
   TrivialExists.
 (* andimm - rolm *)
-  destruct (Int.eq mask1 (Int.not mask2) && is_rlw_mask mask2) as []_eqn.
+  destruct (Int.eq mask1 (Int.not mask2) && is_rlw_mask mask2) eqn:?.
   destruct (andb_prop _ _ Heqb0). 
   generalize (Int.eq_spec mask1 (Int.not mask2)); rewrite H1; intros.
   InvEval. subst. TrivialExists. 
   TrivialExists.
 (* rolm - andimm *)
-  destruct (Int.eq mask2 (Int.not mask1) && is_rlw_mask mask1) as []_eqn.
+  destruct (Int.eq mask2 (Int.not mask1) && is_rlw_mask mask1) eqn:?.
   destruct (andb_prop _ _ Heqb0). 
   generalize (Int.eq_spec mask2 (Int.not mask1)); rewrite H1; intros.
   InvEval. subst. rewrite Val.or_commut. TrivialExists.
@@ -507,7 +507,7 @@ Theorem eval_divuimm:
   exists v, eval_expr ge sp e m le (divuimm a n) v /\ Val.lessdef z v.
 Proof.
   intros; unfold divuimm. 
-  destruct (Int.is_power2 n) as []_eqn. 
+  destruct (Int.is_power2 n) eqn:?. 
   replace z with (Val.shru x (Vint i)). apply eval_shruimm; auto.
   eapply Val.divu_pow2; eauto.
   TrivialExists. 
@@ -533,7 +533,7 @@ Theorem eval_moduimm:
   exists v, eval_expr ge sp e m le (moduimm a n) v /\ Val.lessdef z v.
 Proof.
   intros; unfold moduimm. 
-  destruct (Int.is_power2 n) as []_eqn. 
+  destruct (Int.is_power2 n) eqn:?. 
   replace z with (Val.and x (Vint (Int.sub n Int.one))). apply eval_andimm; auto.
   eapply Val.modu_pow2; eauto.
   exploit Val.modu_divu; eauto. intros [v [A B]].
@@ -758,7 +758,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).
@@ -770,7 +770,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.