From 0b417c12eb10bb29bcee04384b6c0855cb9de73a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 5 Oct 2016 17:50:45 +0200
Subject: unification.ml: fix for bug #4763, unif regression

Do not force all remaining conversions problems to be solved after the
_first_ solution of an evar, but only at the end of assignment of terms
to evars in w_merge. This was hell to track down, thanks for the help of
Maxime. contribs pass and HoTT too.
---
 pretyping/evarsolve.ml   | 2 ++
 pretyping/unification.ml | 3 +--
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 0db309f948..4084ee579a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1580,6 +1580,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 347bf6f9e5..3d734ea9a9 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1244,8 +1244,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]
-- 
cgit v1.2.3


From 08f4cfc9dfb03973ae652ef6576342ae38f8f199 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 6 Oct 2016 11:21:10 +0200
Subject: w_merge: Add a comment about the (List.rev evars)

This change exposed bug #4763
---
 pretyping/unification.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3d734ea9a9..b7edd6fcd6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1361,7 +1361,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
-- 
cgit v1.2.3


From 0a6f0c161756a1878dd81e438df86f08631d8399 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 6 Oct 2016 11:38:06 +0200
Subject: evarconv.ml: Fix bug #4529, primproj unfolding

Evarconv was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
---
 pretyping/evarconv.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index aead1cb35f..0d261f7f87 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -39,12 +39,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 =
-- 
cgit v1.2.3