Merge branch 'v8.5' into v8.6

5 files changed, 65 insertions, 9 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b033f5a39..b7e0535da 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -42,12 +42,7 @@ let _ = Goptions.declare_bool_option {
 let unfold_projection env evd ts p c =
   let cst = Projection.constant p in
     if is_transparent_constant ts cst then
-      let c' = Some (mkProj (Projection.make cst true, c)) in
-	match ReductionBehaviour.get (Globnames.ConstRef cst) with
-	| None -> c'
-	| Some (recargs, nargs, flags) ->
-	  if (List.mem `ReductionNeverUnfold flags) then None
-	  else c'
+      Some (mkProj (Projection.make cst true, c))
     else None
       
 let eval_flexible_term ts env evd c =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6c8677855..a97e248ae 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1591,6 +1591,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
  * ass.
  *)
 
+(* This criterion relies on the fact that we postpone only problems of the form:
+?x [?x1 ... ?xn] = t or the symmetric case. *)
 let status_changed lev (pbty,_,t1,t2) =
   (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) ||
   (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e6f4090f4..531b61553 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1269,8 +1269,7 @@ let solve_simple_evar_eqn ts env evd ev rhs =
   match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
   | UnifFailure (evd,reason) ->
       error_cannot_unify env evd ~reason (mkEvar ev,rhs);
-  | Success evd ->
-      Evarconv.consider_remaining_unif_problems env evd
+  | Success evd -> evd
 
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]
@@ -1389,7 +1388,9 @@ let w_merge env with_types flags (evd,metas,evars) =
     in w_merge_rec evd [] [] eqns
   in
   let res =  (* merge constraints *)
-    w_merge_rec evd (order_metas metas) (List.rev evars) []
+    w_merge_rec evd (order_metas metas)
+                (* Assign evars in the order of assignments during unification *)
+                (List.rev evars) []
   in
     if with_types then check_types res
     else res
diff --git a/test-suite/bugs/closed/4529.v b/test-suite/bugs/closed/4529.v
new file mode 100644
index 000000000..8b3c24fec
--- /dev/null
+++ b/test-suite/bugs/closed/4529.v
@@ -0,0 +1,45 @@
+(* File reduced by coq-bug-finder from original input, then from 1334 lines to 1518 lines, then from 849 lines to 59 lines *)
+(* coqc version 8.5 (January 2016) compiled on Jan 22 2016 18:20:47 with OCaml 4.02.3
+   coqtop version r-schnelltop:/home/r/src/coq/coq,(HEAD detached at V8.5) (5e23fb90b39dfa014ae5c4fb46eb713cca09dbff) *)
+Require Coq.Setoids.Setoid.
+Import Coq.Setoids.Setoid.
+
+Class Equiv A := equiv: relation A.
+Infix "≡" := equiv (at level 70, no associativity).
+Notation "(≡)" := equiv (only parsing).
+
+(* If I remove this line, everything compiles. *)
+Set Primitive Projections.
+
+Class Dist A := dist : nat -> relation A.
+Notation "x ={ n }= y" := (dist n x y)
+  (at level 70, n at next level, format "x  ={ n }=  y").
+
+Record CofeMixin A `{Equiv A, Dist A} := {
+  mixin_equiv_dist x y : x ≡ y <-> forall n, x ={n}= y;
+  mixin_dist_equivalence n : Equivalence (dist n);
+}.
+
+Structure cofeT := CofeT {
+  cofe_car :> Type;
+  cofe_equiv : Equiv cofe_car;
+  cofe_dist : Dist cofe_car;
+  cofe_mixin : CofeMixin cofe_car
+}.
+Existing Instances cofe_equiv cofe_dist.
+Arguments cofe_car : simpl never.
+
+Section cofe_mixin.
+  Context {A : cofeT}.
+  Implicit Types x y : A.
+  Lemma equiv_dist x y : x ≡ y <-> forall n, x ={n}= y.
+Admitted.
+End cofe_mixin.
+  Context {A : cofeT}.
+  Global Instance cofe_equivalence : Equivalence ((≡) : relation A).
+  Proof.
+    split.
+    *
+ intros x.
+apply equiv_dist.
+
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
new file mode 100644
index 000000000..ae8ed0e6e
--- /dev/null
+++ b/test-suite/bugs/closed/4763.v
@@ -0,0 +1,13 @@
+Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses.
+Coercion is_true : bool >-> Sortclass.
+Global Instance: Transitive leb.
+Admitted.
+
+Goal forall x y z, leb x y -> leb y z -> True.
+  intros ??? H H'.
+  lazymatch goal with
+  | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ]
+    => pose proof (transitivity H H' : is_true (R x z))
+  end.
+  exact I.
+Qed.
\ No newline at end of file