Merge branch 'v8.6'

5 files changed, 13 insertions, 11 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b7fc2de95..51d006e25 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -45,12 +45,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 a744f5ec6..c44903e8c 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/program.ml b/pretyping/program.ml
index b4333847b..4b6137b53 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -15,10 +15,12 @@ open Term
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
 let find_reference locstr dir s =
-  let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
+  let dp = make_dir dir in
+  let sp = Libnames.make_path dp (Id.of_string s) in
   try Nametab.global_of_path sp
   with Not_found ->
-    anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp)
+    user_err (str "Library " ++ Libnames.pr_dirpath dp ++
+      str " has to be required first.")
 
 let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
 let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index e4cca2679..8ca40f829 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -46,3 +46,5 @@ val type_of_global_reference_knowing_conclusion :
 val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list
 
 val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
+
+val print_retype_error : retype_error -> Pp.std_ppcmds
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5d6c41103..a96a496b8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1270,8 +1270,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]
@@ -1390,7 +1389,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