Merge branch 'v8.6'

4 files changed, 26 insertions, 21 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3f01adf7e3..934cefbfe7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -65,13 +65,14 @@ let error_wrong_numarg_constructor ?loc env c n =
 let error_wrong_numarg_inductive ?loc env c n =
   raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n))
 
-let rec list_try_compile f = function
-  | [a] -> f a
-  | [] -> anomaly (str "try_find_f")
+let list_try_compile f l =
+  let rec aux errors = function
+  | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors)
   | h::t ->
       try f h
-      with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ ->
-	    list_try_compile f t
+      with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
+	    aux (e::errors) t in
+  aux [] l
 
 let force_name =
   let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6e5ded1523..bafb009f52 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1599,8 +1599,6 @@ 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/pretyping.ml b/pretyping/pretyping.ml
index 1602f4262a..2f13121ad1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -249,17 +249,24 @@ type inference_flags = {
   expand_evars : bool
 }
 
-let frozen_holes (sigma, sigma') =
-  (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma)
-
-let pending_holes (sigma, sigma') =
-  let fold evk _ accu =
-    if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu
-  in
-  Evd.fold_undefined fold sigma' Evar.Set.empty
+(* Compute the set of still-undefined initial evars up to restriction
+   (e.g. clearing) and the set of yet-unsolved evars freshly created
+   in the extension [sigma'] of [sigma] (excluding the restrictions of
+   the undefined evars of [sigma] to be freshly created evars of
+   [sigma']). Otherwise said, we partition the undefined evars of
+   [sigma'] into those already in [sigma] or deriving from an evar in
+   [sigma] by restriction, and the evars properly created in [sigma'] *)
+
+let frozen_and_pending_holes (sigma, sigma') =
+  let add_derivative_of evk evi acc =
+    match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
+  let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in
+  let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
+  let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
+  (frozen,pending)
 
 let apply_typeclasses env evdref frozen fail_evar =
-  let filter_frozen = frozen in
+  let filter_frozen evk = Evar.Set.mem evk frozen in
   evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
 	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
@@ -327,8 +334,7 @@ let check_evars_are_solved env current_sigma frozen pending =
 (* Try typeclasses, hooks, unification heuristics ... *)
 
 let solve_remaining_evars flags env current_sigma pending =
-  let frozen = frozen_holes pending in
-  let pending = pending_holes pending in
+  let frozen,pending = frozen_and_pending_holes pending in
   let evdref = ref current_sigma in
   if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
   if Option.has_some flags.use_hook then
@@ -338,8 +344,7 @@ let solve_remaining_evars flags env current_sigma pending =
   !evdref
 
 let check_evars_are_solved env current_sigma pending =
-  let frozen = frozen_holes pending in
-  let pending = pending_holes pending in
+  let frozen,pending = frozen_and_pending_holes pending in
   check_evars_are_solved env current_sigma frozen pending
 
 let process_inference_flags flags env initial_sigma (sigma,c) =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a96a496b84..e73c5ffaf3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1270,7 +1270,8 @@ 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 -> evd
+  | Success evd ->
+      Evarconv.consider_remaining_unif_problems env evd
 
 (* [w_merge env sigma b metas evars] merges common instances in metas
    or in evars, possibly generating new unification problems; if [b]