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, 43 insertions, 37 deletions

diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 8ee9c2e..b0598e9 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -1087,7 +1087,8 @@ Proof.
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto.
   intros A.
   exploit transl_cond_correct. eauto. eauto. 
-  instantiate (1 := rs). instantiate (1 := m'). unfold PregEq.t. rewrite A. 
+  instantiate (1 := rs). instantiate (1 := m').
+  rewrite A || (unfold PregEq.t; rewrite A).
   intros [rs2 [EX [RES OTH]]]. 
   inv AT. simpl in H5.
   generalize (functions_transl _ _ H4); intro FN.
@@ -1123,7 +1124,8 @@ Proof.
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto.
   intros A.
   exploit transl_cond_correct. eauto. 
-  instantiate (1 := rs). instantiate (1 := m'). unfold PregEq.t. rewrite A. 
+  instantiate (1 := rs). instantiate (1 := m').
+  rewrite A || (unfold PregEq.t; rewrite A).
   intros [rs2 [EX [RES OTH]]].
   left; eapply exec_straight_steps; eauto with coqlib.
   exists m'; split; auto.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index e7d2509..19edcd9 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -539,7 +539,7 @@ Proof.
     auto.
     rewrite IHl. rewrite DISTR. decEq. decEq. auto.
   intros. unfold decompose_int. 
-  destruct (decompose_int_rec 12 n Int.zero) as []_eqn. 
+  destruct (decompose_int_rec 12 n Int.zero) eqn:?. 
   simpl. exploit decompose_int_rec_nil; eauto. congruence.
   simpl. rewrite B. decEq.  
   generalize (DECOMP 12%nat n Int.zero Int.zero).
@@ -617,7 +617,7 @@ Lemma iterate_op_correct:
 Proof.
   intros until k; intros SEM2 SEM1.
   unfold iterate_op.
-  destruct (decompose_int n) as [ | i tl] _eqn.
+  destruct (decompose_int n) as [ | i tl] eqn:?.
   unfold decompose_int in Heql. destruct (decompose_int_rec 12%nat n Int.zero); congruence.
   revert k. pattern tl. apply List.rev_ind.
   (* base case *)
@@ -1256,7 +1256,7 @@ Proof.
   eapply exec_straight_trans. eauto. 
   apply exec_straight_two with rs2 m; auto.
   simpl. unfold rs3, v. 
-  destruct (rs2 (crbit_for_cond c)) as []_eqn; auto.
+  destruct (rs2 (crbit_for_cond c)) eqn:?; auto.
   destruct (Int.eq i Int.zero); auto. 
   decEq. decEq. apply extensionality; intros. unfold Pregmap.set.
   destruct (PregEq.eq x (ireg_of res)); auto. subst. 
@@ -1380,6 +1380,7 @@ Lemma transl_load_int_correct:
 Proof.
   intros. unfold transl_load_store_int.
   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.
@@ -1421,6 +1422,7 @@ Lemma transl_load_float_correct:
 Proof.
   intros. unfold transl_load_store_int.
   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.
@@ -1455,7 +1457,8 @@ Lemma transl_store_int_correct:
     /\ agree (undef_temps ms) sp rs'.
 Proof.
   intros. unfold transl_load_store_int.
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto.
+  unfold PregEq.t. 
   intros [a' [A B]].
   exploit preg_val; eauto. instantiate (1 := rd). intros C.
   exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]].
@@ -1498,7 +1501,8 @@ Lemma transl_store_float_correct:
     /\ agree (undef_temps ms) sp rs'.
 Proof.
   intros. unfold transl_load_store_float.
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. 
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto.
+  unfold PregEq.t. 
   intros [a' [A B]].
   exploit preg_val; eauto. instantiate (1 := rd). intros C.
   exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]].
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 4c38d5e..e7e6a41 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -149,7 +149,7 @@ Proof.
   destruct (propagate_float_constants tt); simpl; auto.
   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.
@@ -247,7 +247,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.
   econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto. 
   econstructor; split; eauto. simpl. congruence.
 Qed.
@@ -261,7 +261,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; intros.
+  destruct (Int.ltu n Int.iwordsize) eqn:?; intros.
   econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto. 
   econstructor; split; eauto. simpl. congruence.
 Qed.
@@ -275,7 +275,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.
   econstructor; split. simpl; eauto.  rewrite mk_shift_amount_eq; auto. 
   econstructor; split; eauto. simpl. congruence.
 Qed.
@@ -291,7 +291,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.
   exploit Int.is_power2_range; eauto. intros R.
   econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto.  
   rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). auto.
@@ -306,8 +306,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.
@@ -321,7 +321,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)). 
   econstructor; split. simpl. rewrite mk_shift_amount_eq. eauto. 
   eapply Int.is_power2_range; eauto. auto.
diff --git a/arm/Op.v b/arm/Op.v
index cfe8b83..f26bccc 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -775,8 +775,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.
@@ -796,8 +796,8 @@ Opaque Int.add.
   eapply CMPU; eauto.
   eapply CMP. eauto. eapply eval_shift_inj. eauto. auto.
   eapply CMPU. eauto. eapply eval_shift_inj. eauto. auto.
-  eapply CMP; eauto. 
-  eapply CMPU; eauto.
+  eapply CMP; try eassumption; eauto.
+  eapply CMPU; try eassumption; eauto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; simpl in H0; inv H0; auto.
@@ -871,7 +871,7 @@ Proof.
   inv H4; simpl in *; inv H1. TrivialExists.
   inv H4; simpl in *; inv H1. 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.
@@ -1005,7 +1005,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/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 6415248..9d09fc1 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -719,7 +719,7 @@ let print_init oc = function
       fprintf oc "	.quad	%Ld %s %.18g\n" (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 "	.word	%a\n" print_symb_ofs (symb, ofs)
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index e25fb0c..ecc758f 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -204,10 +204,10 @@ Opaque mk_shift_amount.
   red; intros until x.  unfold shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl.
+  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl.
   destruct (shlimm_match a); intros.
   InvEval. simpl; rewrite Heqb. TrivialExists.
-  destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn.
+  destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   InvEval. subst x. exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp.
   simpl. rewrite mk_shift_amount_eq; auto. 
   destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0.
@@ -224,10 +224,10 @@ Proof.
   red; intros until x.  unfold shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl.
+  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl.
   destruct (shrimm_match a); intros.
   InvEval. simpl; rewrite Heqb. TrivialExists.
-  destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn.
+  destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   InvEval. subst x. exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp.
   simpl. rewrite mk_shift_amount_eq; auto. 
   destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0.
@@ -244,13 +244,13 @@ Proof.
   red; intros until x.  unfold shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
-  destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl.
+  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl.
   destruct (shruimm_match a); intros.
   InvEval. simpl; rewrite Heqb. TrivialExists.
-  destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn.
+  destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
   InvEval. subst x. exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp.
   simpl. rewrite mk_shift_amount_eq; auto. 
-  destruct v1; simpl; auto. destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto.
+  destruct v1; simpl; auto. destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
   rewrite Heqb; rewrite Heqb0. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto.
   TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. 
   TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. 
@@ -379,27 +379,27 @@ Proof.
   rewrite Val.or_commut. apply eval_orimm; auto.
   apply eval_orimm; auto.
 (* shl - shru *)
-  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.
   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.
   subst. TrivialExists.
   econstructor. EvalOp. simpl; eauto. econstructor; eauto. constructor.
   simpl. auto.
 (* shru - shr *)
-  destruct (Int.eq (Int.add n2 n1) Int.iwordsize && same_expr_pure t1 t2) as []_eqn.
+  destruct (Int.eq (Int.add n2 n1) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
   destruct (andb_prop _ _ Heqb0).
   generalize (Int.eq_spec (Int.add n2 n1) Int.iwordsize); rewrite H1; intros.
   exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. 
   exists (Val.ror v0 (Vint n1)); 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_commut. rewrite <- Int.or_ror; auto.
   subst. TrivialExists.
   econstructor. EvalOp. simpl; eauto. econstructor; eauto. constructor.
@@ -490,7 +490,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. 
@@ -516,7 +516,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))). TrivialExists.
   eapply Val.modu_pow2; eauto.
   exploit Val.modu_divu; eauto. intros [v [A B]].