Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into maximedenes-coq-8.6

9 files changed, 22 insertions, 19 deletions

diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 52f1f112..fa402e9f 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -978,7 +978,8 @@ Ltac UseTransfer :=
   eapply match_succ_states; eauto. simpl; auto.
   destruct res; auto. apply eagree_set_undef; auto.
   eapply magree_storebytes_left; eauto.
-  exploit aaddr_arg_sound; eauto. 
+  clear H3.
+  exploit aaddr_arg_sound; eauto.
   intros (bc & A & B & C).
   intros. eapply nlive_contains; eauto.
   erewrite Mem.loadbytes_length in H0 by eauto.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index d06fa997..d5d7e033 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -1171,11 +1171,11 @@ Proof.
   rewrite <- SP in MS0.
   eapply match_stacks_invariant; eauto.
     intros. destruct (eq_block b1 stk).
-    subst b1. rewrite D in H8; inv H8. subst b2. eelim Plt_strict; eauto.
+    subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto.
     rewrite E in H8; auto.
     intros. exploit Mem.perm_alloc_inv. eexact H. eauto.
     destruct (eq_block b1 stk); intros; auto.
-    subst b1. rewrite D in H8; inv H8. subst b2. eelim Plt_strict; eauto.
+    subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto.
     intros. eapply Mem.perm_alloc_1; eauto.
     intros. exploit Mem.perm_alloc_inv. eexact A. eauto.
     rewrite dec_eq_false; auto.
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index a53040f9..8e8b9c0b 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -1255,8 +1255,8 @@ Proof.
   split; simpl; auto; intros.
   rewrite PTree.gsspec in H6. destruct (peq id0 id).
 + inv H6. destruct H3. congruence. destruct gl!id as [iv0|] eqn:NG.
-  rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto.
-  rewrite ISet.In_interval. omega.
+  unfold iv'; rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto.
+  unfold iv'; rewrite ISet.In_interval. omega.
 + eauto.
 - (* Stk ofs *)
   split; simpl; auto; intros. destruct H3.
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 7e9c3ca0..c79ae4fd 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -1015,7 +1015,7 @@ Proof.
   { rewrite STK, TSTK.
     apply match_stacks_incr with j; auto.
     intros. destruct (eq_block b1 stk).
-    subst b1. rewrite F in H1; inv H1. subst b2. split; apply Ple_refl.
+    subst b1. rewrite F in H1; inv H1. split; apply Ple_refl.
     rewrite G in H1 by auto. congruence. }
   econstructor; split.
   eapply exec_function_internal; eauto.
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 4dcf2a47..a9ffcd3d 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -130,8 +130,8 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
 
 Ltac mydestr :=
   match goal with
-  | [ |- None = Some _ -> _ ] => intro X; discriminate
-  | [ |- Some _ = Some _ -> _ ] => intro X; inv X
+  | [ |- None = Some _ -> _ ] => let X := fresh "X" in intro X; discriminate
+  | [ |- Some _ = Some _ -> _ ] => let X := fresh "X" in intro X; inv X
   | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
   | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
   | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
@@ -2038,12 +2038,14 @@ Definition do_step (w: world) (s: state) : list transition :=
 
 Ltac myinv :=
   match goal with
-  | [ |- In _ nil -> _ ] => intro X; elim X
+  | [ |- In _ nil -> _ ] => let X := fresh "X" in intro X; elim X
   | [ |- In _ (ret _ _) -> _ ] =>
+        let X := fresh "X" in
         intro X; elim X; clear X;
-        [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
+        [let EQ := fresh "EQ" in intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
   | [ |- In _ (_ :: nil) -> _ ] =>
-        intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv]
+        let X := fresh "X" in
+        intro X; elim X; clear X; [let EQ := fresh "EQ" in intro EQ; inv EQ; myinv | myinv]
   | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv
   | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv
   | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 0794743d..8d6cdb24 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -1064,7 +1064,7 @@ Proof.
     destruct (complete_members env m) eqn:C; simplify_eq EQ. clear EQ; intros EQ.
     rewrite PTree.gsspec. intros [A|A]; auto.
     destruct (peq id id0); auto.
-    inv A. rewrite <- H1; auto.
+    inv A. rewrite <- H0; auto.
   }
   intros. exploit REC; eauto. rewrite PTree.gempty. intuition congruence.
 Qed.
@@ -1519,7 +1519,7 @@ Local Transparent Linker_program.
   - intros. exploit link_match_fundef; eauto. intros (tf & A & B). exists tf; auto.
   - intros.
     Local Transparent Linker_types.
-    simpl in *. destruct (type_eq v1 v2); inv H4. subst v tv2. exists tv1; rewrite dec_eq_true; auto.
+    simpl in *. destruct (type_eq v1 v2); inv H4. exists v; rewrite dec_eq_true; auto.
   - eauto.
   - eauto.
   - eauto.
diff --git a/configure b/configure
index eacc28d3..182e086a 100755
--- a/configure
+++ b/configure
@@ -407,15 +407,15 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
-  8.5pl2|8.5pl3)
+  8.6)
         echo "version $coq_ver -- good!";;
   ?.*)
         echo "version $coq_ver -- UNSUPPORTED"
-        echo "Error: CompCert requires Coq version 8.5pl2."
+        echo "Error: CompCert requires Coq version 8.6."
         missingtools=true;;
   *)
         echo "NOT FOUND"
-        echo "Error: make sure Coq version 8.5pl2 is installed."
+        echo "Error: make sure Coq version 8.6 is installed."
         missingtools=true;;
 esac
 
@@ -448,7 +448,7 @@ else
   ocaml_opt_comp=false
 fi
 
-MENHIR_REQUIRED=20160303
+MENHIR_REQUIRED=20161201
 echo "Testing Menhir... " | tr -d '\n'
 menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'`
 case "$menhir_ver" in
diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v
index 23999a50..a4accfa5 100644
--- a/flocq/Appli/Fappli_IEEE.v
+++ b/flocq/Appli/Fappli_IEEE.v
@@ -1,3 +1,4 @@
+Unset Bracketing Last Introduction Pattern.
 (**
 This file is part of the Flocq formalization of floating-point
 arithmetic in Coq: http://flocq.gforge.inria.fr/
diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v
index d40c1a09..7d1d490a 100644
--- a/flocq/Core/Fcore_digits.v
+++ b/flocq/Core/Fcore_digits.v
@@ -853,8 +853,7 @@ Proof.
 intros n Zn.
 rewrite <- (Zdigits_abs n).
 assert (Hn: (0 < Zabs n)%Z).
-destruct n ; try easy.
-now elim Zn.
+destruct n ; now easy.
 destruct (Zabs n) as [|p|p] ; try easy ; clear.
 simpl.
 generalize 1%Z (radix_val beta) (refl_equal Lt : (0 < 1)%Z).