From 379c2403b1cd031091a2271353f26ab24afeb1e5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 22 Oct 2016 10:17:39 +0200
Subject: Port fix for bugs 4763, 5149, previously 0b417c12e

Adds a compatibility flag so that the behavior of 8.5 can be obtained too.

Original commit:
   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. This was hell to track down, thanks
    for the help of Maxime. contribs pass and HoTT too.
---
 pretyping/unification.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e0a81cfbb9..cec9f700af 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1270,7 +1270,11 @@ let solve_simple_evar_eqn ts env evd ev rhs =
   | UnifFailure (evd,reason) ->
       error_cannot_unify env evd ~reason (mkEvar ev,rhs);
   | Success evd ->
-      Evarconv.consider_remaining_unif_problems env evd
+     if Flags.version_less_or_equal Flags.V8_5 then
+       (* We used to force solving unrelated problems at arbitrary times *)
+       Evarconv.consider_remaining_unif_problems env evd
+     else (* solve_simple_eqn calls reconsider_conv_pbs itself *)
+       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 ccb173a440fa2eb7105a692c979253edbfe475ee Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 19 Oct 2016 13:33:28 +0200
Subject: Unification constraint handling (#4763, #5149)

Refine fix for bug #4763, fixing #5149

Tactic [Refine.solve_constraints] and global option

Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.

Fix test-suite files too.
---
 pretyping/unification.ml | 19 +++++--------------
 1 file changed, 5 insertions(+), 14 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index cec9f700af..fc63015a8e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1301,7 +1301,6 @@ let w_merge env with_types flags (evd,metas,evars) =
 	      if is_mimick_head flags.modulo_delta f then
 		let evd' =
 		  mimick_undefined_evar evd flags f (Array.length cl) evk in
-		(* let evd' = Evarconv.consider_remaining_unif_problems env evd' in *)
 		  w_merge_rec evd' metas evars eqns
 	      else
 		let evd' = 
@@ -1397,8 +1396,7 @@ let w_merge env with_types flags (evd,metas,evars) =
                 (* Assign evars in the order of assignments during unification *)
                 (List.rev evars) []
   in
-    if with_types then check_types res
-    else res
+  if with_types then check_types res else res
 
 let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
   let metas,evd = retract_coercible_metas evd in
@@ -1456,7 +1454,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 =
   let subst = Array.fold_left2 fold_subst subst l1 l2 in
   let evd = w_merge env true flags.merge_unify_flags subst in
   try_resolve_typeclasses env evd flags.resolve_evars
-    (mkApp(f1,l1)) (mkApp(f2,l2))
+                          (mkApp(f1,l1)) (mkApp(f2,l2))
 
 (* takes a substitution s, an open term op and a closed term cl
    try to find a subterm of cl which matches op, if op is just a Meta
@@ -1885,21 +1883,14 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
     error_wrong_abstraction_type env evd'
       (Evd.meta_name evd p) pred typp predtyp;
   w_merge env false flags.merge_unify_flags
-    (evd',[p,pred,(Conv,TypeProcessed)],[])
-
-  (* let evd',metas,evars =  *)
-  (*   try unify_0 env evd' CUMUL flags predtyp typp  *)
-  (*   with NotConvertible -> *)
-  (*     error_wrong_abstraction_type env evd *)
-  (*       (Evd.meta_name evd p) pred typp predtyp *)
-  (* in *)
-  (*   w_merge env false flags (evd',(p,pred,(Conv,TypeProcessed))::metas,evars) *)
+          (evd',[p,pred,(Conv,TypeProcessed)],[])
 
 let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
   let typp = Typing.meta_type evd p in
   let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
   w_merge env false flags.merge_unify_flags
-    (evd,[p,pred,(Conv,TypeProcessed)],[])
+          (evd,[p,pred,(Conv,TypeProcessed)],[])
+
 
 let secondOrderAbstractionAlgo dep =
   if dep then secondOrderDependentAbstraction else secondOrderAbstraction
-- 
cgit v1.2.3


From be11ab322fa73804118738e7a08e9910fdf4600d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 22 Oct 2016 11:03:13 +0200
Subject: Renamings to avoid confusion deprecating old names

reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
---
 pretyping/evarconv.ml    | 8 +++++---
 pretyping/evarconv.mli   | 3 +++
 pretyping/evarsolve.ml   | 6 ++++--
 pretyping/evarsolve.mli  | 3 +++
 pretyping/pretyping.ml   | 2 +-
 pretyping/unification.ml | 6 +++---
 6 files changed, 19 insertions(+), 9 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3680cd777a..07f6d9d383 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1081,7 +1081,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
               match evar_conv_x ts env_evar evd CUMUL idty evty with
               | UnifFailure _ -> error "Cannot find an instance"
               | Success evd ->
-              match reconsider_conv_pbs (evar_conv_x ts) evd with
+              match reconsider_unif_constraints (evar_conv_x ts) evd with
               | UnifFailure _ -> error "Cannot find an instance"
               | Success evd ->
               evd
@@ -1208,7 +1208,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
             let conv_algo = evar_conv_x ts in
             let evd = check_evar_instance evd evk a conv_algo in
             let evd = Evd.define evk a evd in
-            match reconsider_conv_pbs conv_algo evd with
+            match reconsider_unif_constraints conv_algo evd with
             | Success evd -> solve_unconstrained_evars_with_candidates ts evd
             | UnifFailure _ -> aux l
           with
@@ -1231,7 +1231,7 @@ let solve_unconstrained_impossible_cases env evd =
 	Evd.define evk ty evd' 
     | _ -> evd') evd evd
 
-let consider_remaining_unif_problems env
+let solve_unif_constraints_with_heuristics env
     ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd =
   let evd = solve_unconstrained_evars_with_candidates ts evd in
   let rec aux evd pbs progress stuck =
@@ -1263,6 +1263,8 @@ let consider_remaining_unif_problems env
   check_problems_are_solved env heuristic_solved_evd;
   solve_unconstrained_impossible_cases env heuristic_solved_evd
 
+let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics
+
 (* Main entry points *)
 
 exception UnableToUnify of evar_map * unification_error
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 14947c8927..2231e5bc30 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -33,7 +33,10 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -
 (** Try heuristics to solve pending unification problems and to solve
     evars with candidates *)
 
+val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
+
 val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map
+(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *)
 
 (** Check all pending unification problems are solved and raise an
     error otherwise *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f1526faccc..f0aa9b564f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1603,7 +1603,7 @@ 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)
 
-let reconsider_conv_pbs conv_algo evd =
+let reconsider_unif_constraints conv_algo evd =
   let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
   List.fold_left
     (fun p (pbty,env,t1,t2 as x) ->
@@ -1616,6 +1616,8 @@ let reconsider_conv_pbs conv_algo evd =
     (Success evd)
     pbs
 
+let reconsider_conv_pbs = reconsider_unif_constraints
+
 (* Tries to solve problem t1 = t2.
  * Precondition: t1 is an uninstantiated evar
  * Returns an optional list of evars that were instantiated, or None
@@ -1626,7 +1628,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
   try
     let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
     let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
-      reconsider_conv_pbs conv_algo evd
+      reconsider_unif_constraints conv_algo evd
   with
     | NotInvertibleUsingOurAlgorithm t ->
         UnifFailure (evd,NotClean (ev1,env,t))
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index f94c83b6dc..b6bdc07889 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -54,7 +54,10 @@ val solve_evar_evar : ?force:bool ->
 val solve_simple_eqn : conv_fun -> ?choose:bool -> env ->  evar_map ->
   bool option * existential * constr -> unification_result
 
+val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
+
 val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
+(** @deprecated Alias for [reconsider_unif_constraints] *)
 
 val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
   constr -> constr list option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6afa55862f..95d854323a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -290,7 +290,7 @@ let apply_inference_hook hook evdref pending =
 
 let apply_heuristics env evdref fail_evar =
   (* Resolve eagerly, potentially making wrong choices *)
-  try evdref := consider_remaining_unif_problems
+  try evdref := solve_unif_constraints_with_heuristics
 	~ts:(Typeclasses.classes_transparent_state ()) env !evdref
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in if fail_evar then iraise e
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fc63015a8e..259318693f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1220,7 +1220,7 @@ let is_mimick_head ts f =
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
   let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in
-  let evd' = Evarconv.consider_remaining_unif_problems env evd' in
+  let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
   let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
     (evd',j'.uj_val)
 
@@ -1272,8 +1272,8 @@ let solve_simple_evar_eqn ts env evd ev rhs =
   | Success evd ->
      if Flags.version_less_or_equal Flags.V8_5 then
        (* We used to force solving unrelated problems at arbitrary times *)
-       Evarconv.consider_remaining_unif_problems env evd
-     else (* solve_simple_eqn calls reconsider_conv_pbs itself *)
+       Evarconv.solve_unif_constraints_with_heuristics env evd
+     else (* solve_simple_eqn calls reconsider_unif_constraints itself *)
        evd
 
 (* [w_merge env sigma b metas evars] merges common instances in metas
-- 
cgit v1.2.3


From d6fe6773c959493ed97108e1032b1bd8c1e78081 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 24 Oct 2016 18:18:33 +0200
Subject: Lets Hints/Instances take an optional pattern

In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
---
 pretyping/typeclasses.ml  | 48 +++++++++++++++++++++++------------------------
 pretyping/typeclasses.mli | 17 +++++++++--------
 2 files changed, 32 insertions(+), 33 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 31ef3dfdd7..b8da6b6852 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -65,7 +65,8 @@ type typeclass = {
   cl_props : Context.Rel.t;
 
   (* The method implementaions as projections. *)
-  cl_projs : (Name.t * (direction * int option) option * constant option) list;
+  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
+	      * constant option) list;
   
   cl_strict : bool;
 
@@ -76,10 +77,9 @@ type typeclasses = typeclass Refmap.t
 
 type instance = {
   is_class: global_reference;
-  is_pri: int option;
+  is_info: Vernacexpr.hint_info_expr;
   (* Sections where the instance should be redeclared,
-     -1 for discard, 0 for none, mutable to avoid redeclarations
-     when multiple rebuild_object happen. *)
+     -1 for discard, 0 for none. *)
   is_global: int;
   is_poly: bool;
   is_impl: global_reference;
@@ -89,15 +89,15 @@ type instances = (instance Refmap.t) Refmap.t
 
 let instance_impl is = is.is_impl
 
-let instance_priority is = is.is_pri
+let hint_priority is = is.is_info.Vernacexpr.hint_priority
 
-let new_instance cl pri glob poly impl =
+let new_instance cl info glob poly impl =
   let global =
     if glob then Lib.sections_depth ()
     else -1
   in
     { is_class = cl.cl_impl;
-      is_pri = pri ;
+      is_info = info ;
       is_global = global ;
       is_poly = poly;
       is_impl = impl }
@@ -274,7 +274,9 @@ let check_instance env sigma c =
       not (Evd.has_undefined evd)
   with e when CErrors.noncritical e -> false
 
-let build_subclasses ~check env sigma glob pri =
+open Vernacexpr
+
+let build_subclasses ~check env sigma glob { hint_priority = pri } =
   let _id = Nametab.basename_of_global glob in
   let _next_id = 
     let i = ref (-1) in 
@@ -297,24 +299,24 @@ let build_subclasses ~check env sigma glob pri =
 	   match b with 
 	   | None -> None
 	   | Some (Backward, _) -> None
-	   | Some (Forward, pri') ->
+	   | Some (Forward, info) ->
 	     let proj = Option.get proj in
 	     let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
 	       if check && check_instance env sigma body then None
 	       else 
-		 let pri = 
-		   match pri, pri' with
+		 let newpri =
+		   match pri, info.hint_priority with
 		   | Some p, Some p' -> Some (p + p')
 		   | Some p, None -> Some (p + 1)
 		   | _, _ -> None
 		 in
-		   Some (ConstRef proj, pri, body)) tc.cl_projs 
+		   Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs
 	in
-	let declare_proj hints (cref, pri, body) =
+	let declare_proj hints (cref, info, body) =
 	  let path' = cref :: path in
 	  let ty = Retyping.get_type_of env sigma body in
 	  let rest = aux pri body ty path' in
-	    hints @ (path', pri, body) :: rest
+	    hints @ (path', info, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
   let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
@@ -368,11 +370,11 @@ let is_local i = Int.equal i.is_global (-1)
 let add_instance check inst =
   let poly = Global.is_polymorphic inst.is_impl in
   add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) 
-    inst.is_pri poly;
+    inst.is_info poly;
   List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
     (is_local inst) pri poly)
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
-       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri)
+       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
 
 let rebuild_instance (action, inst) =
   let () = match action with
@@ -404,26 +406,22 @@ let remove_instance i =
   Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
   remove_instance_hint i.is_impl
 
-let declare_instance pri local glob =
+let declare_instance info local glob =
   let ty = Global.type_of_global_unsafe glob in
+  let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr ty with
     | Some (rels, ((tc,_), args) as _cl) ->
-      add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob)
-(*       let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *)
-(*       let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *)
-(* 	Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *)
-(* 	Auto.add_hints local [typeclasses_db]  *)
-(* 	(Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *)
+      add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
     | None -> ()
 
 let add_class cl =
   add_class cl;
   List.iter (fun (n, inst, body) ->
 	     match inst with
-	     | Some (Backward, pri) ->
+	     | Some (Backward, info) ->
 	       (match body with
 	       | None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
-	       | Some b -> declare_instance pri false (ConstRef b))
+	       | Some b -> declare_instance (Some info) false (ConstRef b))
 	     | _ -> ())
   cl.cl_projs
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2530f5dfae..620bc367bd 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -32,7 +32,7 @@ type typeclass = {
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (Name.t * (direction * int option) option * constant option) list;
+  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list;
 
   (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
@@ -50,7 +50,7 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic -> 
+val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
   global_reference -> instance
 val add_instance : instance -> unit
 val remove_instance : instance -> unit
@@ -71,7 +71,7 @@ val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr
   
 val instance_impl : instance -> global_reference
 
-val instance_priority : instance -> int option
+val hint_priority : instance -> int option
 
 val is_class : global_reference -> bool
 val is_instance : global_reference -> bool
@@ -113,21 +113,22 @@ val classes_transparent_state : unit -> transparent_state
 
 val add_instance_hint_hook : 
   (global_reference_or_constr -> global_reference list ->
-   bool (* local? *) -> int option -> Decl_kinds.polymorphic -> unit) Hook.t
+   bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
 val remove_instance_hint_hook : (global_reference -> unit) Hook.t
 val add_instance_hint : global_reference_or_constr -> global_reference list -> 
-  bool -> int option -> Decl_kinds.polymorphic -> unit
+  bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t
 
-val declare_instance : int option -> bool -> global_reference -> unit
+val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.
     check tells if we should check for existence of the 
     subinstances and add only the missing ones. *)
 
-val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
-  (global_reference list * int option * constr) list
+val build_subclasses : check:bool -> env -> evar_map -> global_reference ->
+		       Vernacexpr.hint_info_expr ->
+		       (global_reference list * Vernacexpr.hint_info_expr * constr) list
-- 
cgit v1.2.3


From e6edb3319c850cc7e30e5c31b0bfbf16c5c1a32c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 7 Nov 2016 08:41:21 +0100
Subject: More explicit name for status of unification constraints.

---
 pretyping/pretyping.ml  | 10 +++++-----
 pretyping/pretyping.mli |  2 +-
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 95d854323a..4b6d10c640 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -243,7 +243,7 @@ type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
   use_typeclasses : bool;
-  use_unif_heuristics : bool;
+  solve_unification_constraints : bool;
   use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
@@ -339,7 +339,7 @@ let solve_remaining_evars flags env current_sigma pending =
   if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
   if Option.has_some flags.use_hook then
     apply_inference_hook (Option.get flags.use_hook env) evdref pending;
-  if flags.use_unif_heuristics then apply_heuristics env evdref false;
+  if flags.solve_unification_constraints then apply_heuristics env evdref false;
   if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
   !evdref
 
@@ -1109,14 +1109,14 @@ let ise_pretype_gen flags env sigma lvar kind c =
 
 let default_inference_flags fail = {
   use_typeclasses = true;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = None;
   fail_evar = fail;
   expand_evars = true }
 
 let no_classes_no_fail_inference_flags = {
   use_typeclasses = false;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = None;
   fail_evar = false;
   expand_evars = true }
@@ -1180,7 +1180,7 @@ let understand_ltac flags env sigma lvar kind c =
 
 let constr_flags = {
   use_typeclasses = true;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = None;
   fail_evar = true;
   expand_evars = true }
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index eead48a549..0f3f7c3c9a 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -51,7 +51,7 @@ type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
   use_typeclasses : bool;
-  use_unif_heuristics : bool;
+  solve_unification_constraints : bool;
   use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
-- 
cgit v1.2.3