Merge branch 'v8.5' into v8.6

7 files changed, 70 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index b2113e0bf9..a9942d3a17 100644
--- a/CHANGES
+++ b/CHANGES
@@ -92,6 +92,7 @@ Critical bugfix
 Other bugfixes
 
 - #4780: Induction with universe polymorphism on was creating ill-typed terms.
+- #4673: regression in setoid_rewrite, unfolding let-ins for type unification.
 - #4754: Regression in setoid_rewrite, allow postponed unification problems to remain.
 - #4769: Anomaly with universe polymorphic schemes defined inside sections.
 - #3886: Program: duplicate obligations of mutual fixpoints
@@ -101,6 +102,8 @@ Changes from V8.5pl1 to V8.5pl2
 
 Critical bugfix
 - Checksums of .vo files dependencies were not correctly checked.
+- Unicode-to-ASCII translation was not injective, leading in a soundness bug in
+  the native compiler.
 
 Other bugfixes
 
diff --git a/configure.ml b/configure.ml
index c8096b9e0f..d152c406ee 100644
--- a/configure.ml
+++ b/configure.ml
@@ -809,7 +809,8 @@ let strip =
 (** * md5sum command *)
 
 let md5sum =
-  if arch = "Darwin" || arch = "FreeBSD" then "md5 -q" else "md5sum"
+  if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"]
+  then "md5 -q" else "md5sum"
 
 
 (** * Documentation : do we have latex, hevea, ... *)
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 6a8bda35d6..919e7b5cdc 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -87,7 +87,7 @@ is restored when the current \emph{section} ends.
 \item {\tt Global Unset {\rm\sl flag}.\comindex{Global Unset}}\\
 This command switches {\rm\sl flag} off.  The original state of
 {\rm\sl flag} is \emph{not} restored at the end of the module. Additionally,
-if set in a file, {\rm\sl flag} is switched on when the file is
+if set in a file, {\rm\sl flag} is switched off when the file is
 {\tt Require}-d.
 \end{Variants}
 
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 18557ab6b4..50b3f2c0a0 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -339,8 +339,11 @@ object(self)
   method private show_goals_aux ?(move_insert=false) () =
     Coq.PrintOpt.set_printing_width proof#width;
     if move_insert then begin
-      buffer#place_cursor ~where:self#get_start_of_input;
-      script#recenter_insert;
+      let dest = self#get_start_of_input in
+      if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin
+        buffer#place_cursor ~where:dest;
+        script#recenter_insert
+      end
     end;
     Coq.bind (Coq.goals ~logger:messages#push ()) (function
     | Fail x -> self#handle_failure_aux ~move_insert x
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index df96cfcf6c..47c78ae5c2 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -591,7 +591,7 @@ let general_rewrite_unif_flags () =
       Unification.modulo_conv_on_closed_terms = Some ts;
       Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
       Unification.modulo_delta = ts;
-      Unification.modulo_delta_types = ts;
+      Unification.modulo_delta_types = full_transparent_state;
       Unification.modulo_betaiota = true }
   in {
     Unification.core_unify_flags = core_flags;
diff --git a/test-suite/bugs/closed/4673.v b/test-suite/bugs/closed/4673.v
new file mode 100644
index 0000000000..1ae5081851
--- /dev/null
+++ b/test-suite/bugs/closed/4673.v
@@ -0,0 +1,57 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 2407 lines to 22 lines, then from 528 lines to 35 lines, then from 331 lines to 42 lines, then from 56 lines to 42 lines, then from 63 lines to 46 lines, then from 60 lines to 46 lines *) (* coqc version 8.5 (February 2016) compiled on Feb 21 2016 15:26:16 with OCaml 4.02.3
+   coqtop version 8.5 (February 2016) *)
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Require Coq.Lists.List.
+Import Coq.Lists.List.
+Import Coq.Classes.Morphisms.
+
+Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs))
+           ls
+  : P ls
+  := match ls with
+     | nil => N
+     | x::xs => C x xs
+     end.
+
+Global Instance list_caset_Proper' {A P}
+  : Proper (eq
+              ==> pointwise_relation _ (pointwise_relation _ eq)
+              ==> eq
+              ==> eq)
+           (@list_caset A (fun _ => P)).
+admit.
+Defined.
+
+Global Instance list_caset_Proper'' {A P}
+  : (Proper (eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> forall_relation (fun _ => eq))
+   (list_caset A (fun _ => P))).
+Admitted.
+
+Goal    forall (Char : Type) (P : forall _ : list bool, Prop) (l : list bool) (l0 : forall _ : forall _ : Char, bool, list bool)
+               
+               (T : Type) (T0 : forall _ : T, Type) (t : T),
+    
+    let predata := t in
+
+    forall (splitdata : T0 predata) (l5 : forall _ : T0 t, list nat) (T1 : Type) (b : forall (_ : T1) (_ : Char), bool)
+           
+           (T2 : Type) (a11 : T2) (xs : list T2) (T3 : Type) (i0 : T3) (P0 : Set) (b1 : forall (_ : nat) (_ : P0), bool)
+           
+           (l2 : forall (_ : forall _ : T1, list bool) (_ : forall _ : P0, list bool) (_ : T2), list bool)
+           
+           (l1 : forall (_ : forall _ : forall _ : Char, bool, list bool) (_ : forall _ : P0, list bool) (_ : T3), list bool)
+           
+           (_ : forall NT : forall _ : P0, list bool, @eq (list bool) (l1 l0 NT i0) (l2 (fun f : T1 => l0 (b f)) NT a11)),
+      
+      P
+        (@list_caset T2 (fun _ : list T2 => list bool) l
+                     (fun (_ : T2) (_ : list T2) => l1 l0 (fun a9 : P0 => @map nat bool (fun x0 : nat => b1 x0 a9) (l5 splitdata)) i0
+) xs).
+  intros.
+  subst predata;
+  let H := match goal with H : forall _, _ = _ |- _ => H end in
+  setoid_rewrite H || fail 0 "too early".
+  Undo.
+  setoid_rewrite H.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d141cd8ec1..c49a97cadb 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -54,7 +54,7 @@ let init_color () =
     Terminal.has_style Unix.stderr &&
     (* emacs compilation buffer does not support colors by default,
        its TERM variable is set to "dumb". *)
-    Unix.getenv "TERM" <> "dumb"
+    try Sys.getenv "TERM" <> "dumb" with Not_found -> false
   in
   if has_color then begin
     let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in