Merge commit 'e6edb33' into v8.6

Was PR#331: Solve_constraints and Set Use Unification Heuristics

31 files changed, 178 insertions, 51 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 855235d2b..c01879765 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1157,10 +1157,6 @@ let tclLIFT = Proof.lift
 let tclCHECKINTERRUPT =
    tclLIFT (NonLogical.make Control.check_for_interrupt)
 
-
-
-
-
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 = struct
   type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 725445251..90be2f90a 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -373,7 +373,6 @@ val mark_as_unsafe : unit tactic
     with given up goals cannot be closed. *)
 val give_up : unit tactic
 
-
 (** {7 Control primitives} *)
 
 (** [tclPROGRESS t] checks the state of the proof after [t]. It it is
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index d0318fb5f..2cca760c3 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -38,7 +38,7 @@ DECLARE PLUGIN "extratactics"
 let with_delayed_uconstr ist c tac =
   let flags = {
     Pretyping.use_typeclasses = false;
-    use_unif_heuristics = true;
+    solve_unification_constraints = true;
     use_hook = Some Pfedit.solve_by_implicit_tactic;
     fail_evar = false;
     expand_evars = true
@@ -342,7 +342,7 @@ END
 
 let constr_flags = {
   Pretyping.use_typeclasses = true;
-  Pretyping.use_unif_heuristics = true;
+  Pretyping.solve_unification_constraints = true;
   Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true }
@@ -370,6 +370,11 @@ TACTIC EXTEND simple_refine
 | [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ]
 END
 
+(* Solve unification constraints using heuristics or fail if any remain *)
+TACTIC EXTEND solve_constraints
+[ "solve_constraints" ] -> [ Refine.solve_constraints ]
+END
+
 (**********************************************************************)
 (* Inversion lemmas (Leminv)                                          *)
 
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 8bc2ffd65..22a2d7fc2 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -43,7 +43,7 @@ END
 let eval_uconstrs ist cs =
   let flags = {
     Pretyping.use_typeclasses = false;
-    use_unif_heuristics = true;
+    solve_unification_constraints = true;
     use_hook = Some Pfedit.solve_by_implicit_tactic;
     fail_evar = false;
     expand_evars = true
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 52208979c..20dbc2be4 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -646,7 +646,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
 
 let constr_flags = {
   use_typeclasses = true;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = Some solve_by_implicit_tactic;
   fail_evar = true;
   expand_evars = true }
@@ -661,21 +661,21 @@ let interp_type = interp_constr_gen IsType
 
 let open_constr_use_classes_flags = {
   use_typeclasses = true;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = Some solve_by_implicit_tactic;
   fail_evar = false;
   expand_evars = true }
 
 let open_constr_no_classes_flags = {
   use_typeclasses = false;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = Some solve_by_implicit_tactic;
   fail_evar = false;
   expand_evars = true }
 
 let pure_open_constr_flags = {
   use_typeclasses = false;
-  use_unif_heuristics = true;
+  solve_unification_constraints = true;
   use_hook = None;
   fail_evar = false;
   expand_evars = false }
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index cf9a42945..ef04bef8e 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -354,7 +354,7 @@ let nf_open_term sigma0 ise c =
   !s', Evd.evar_universe_context s, c'
 
 let unif_end env sigma0 ise0 pt ok =
-  let ise = Evarconv.consider_remaining_unif_problems env ise0 in
+  let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
   let s, uc, t = nf_open_term sigma0 ise pt in
   let ise1 = create_evar_defs s in
   let ise1 = Evd.set_universe_context ise1 uc in
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 74a603e51..288a04e60 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -213,7 +213,7 @@ val assert_done : 'a option ref -> 'a
 
 (** Very low level APIs.
     these are calls to evarconv's [the_conv_x] followed by
-    [consider_remaining_unif_problems] and [resolve_typeclasses].
+    [solve_unif_constraints_with_heuristics] and [resolve_typeclasses].
     In case of failure they raise [NoMatch] *)
 
 val unify_HO : env -> evar_map -> constr -> constr -> evar_map
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 28600ad15..9fd55a488 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
@@ -1213,7 +1213,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
@@ -1236,7 +1236,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 =
@@ -1266,6 +1266,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 14947c892..2231e5bc3 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 f1526facc..f0aa9b564 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 f94c83b6d..b6bdc0788 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 6afa55862..4b6d10c64 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
@@ -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
@@ -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 eead48a54..0f3f7c3c9 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
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e0a81cfbb..259318693 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)
 
@@ -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.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
    or in evars, possibly generating new unification problems; if [b]
@@ -1297,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' = 
@@ -1393,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
@@ -1452,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
@@ -1881,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
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 5f0cc73d2..29cad0635 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -46,7 +46,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
   let sigma',typed_c =
     let flags = {
       Pretyping.use_typeclasses = true;
-      Pretyping.use_unif_heuristics = true;
+      Pretyping.solve_unification_constraints = true;
       Pretyping.use_hook = None;
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a3ece1913..eddbf72a8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -13,6 +13,17 @@ open Entries
 open Environ
 open Evd
 
+let use_unification_heuristics_ref = ref true
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname = "Solve unification constraints at every \".\"";
+  Goptions.optkey = ["Solve";"Unification";"Constraints"];
+  Goptions.optread = (fun () -> !use_unification_heuristics_ref);
+  Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a);
+}
+
+let use_unification_heuristics () = !use_unification_heuristics_ref
+
 let refining = Proof_global.there_are_pending_proofs
 let check_no_pending_proofs = Proof_global.check_no_pending_proof
 
@@ -119,6 +130,11 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
       | Vernacexpr.SelectAll -> tac
     in
+    let tac =
+      if use_unification_heuristics () then
+        Proofview.tclTHEN tac Refine.solve_constraints
+      else tac
+    in
     let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
     let () =
       match info_lvl with
diff --git a/proofs/refine.ml b/proofs/refine.ml
index e5114a2ec..3f5527060 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -149,3 +149,14 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
   } in
   refine ?unsafe f
 end }
+
+(** {7 solve_constraints}
+
+  Ensure no remaining unification problems are left. Run at every "." by default. *)
+
+let solve_constraints =
+  let open Proofview in
+  tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
+   try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
+       Unsafe.tclEVARSADVANCE sigma
+   with e -> tclZERO e
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 3d140f036..a44632eff 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -43,3 +43,8 @@ val with_type : Environ.env -> Evd.evar_map ->
 val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)
+
+(** {7 Unification constraint handling} *)
+
+val solve_constraints : unit tactic
+(** Solve any remaining unification problems, applying heuristics. *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 51bf69e5c..af1ab4197 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1440,7 +1440,7 @@ let initial_select_evars filter =
 
 let resolve_typeclass_evars debug depth unique env evd filter split fail =
   let evd =
-    try Evarconv.consider_remaining_unif_problems
+    try Evarconv.solve_unif_constraints_with_heuristics
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
     with e when CErrors.noncritical e -> evd
   in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e9d08d737..bb3cbad92 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1163,7 +1163,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       let dflt_typ = unsafe_type_of env sigma dflt in
       try
 	let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
-	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
+	let () =
+          evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
 	error "Cannot solve a unification problem."
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index af52c5237..db19d54bd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1141,7 +1141,7 @@ let run_delayed env sigma c =
 
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
-  Pretyping.use_unif_heuristics = true;
+  Pretyping.solve_unification_constraints = true;
   Pretyping.use_hook = Some solve_by_implicit_tactic;
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v
index 0be859edd..7fae32871 100644
--- a/test-suite/bugs/closed/2310.v
+++ b/test-suite/bugs/closed/2310.v
@@ -14,4 +14,8 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
    (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
    leave P as subgoal or choose itself one solution *)
 
-intros. refine (Cons (cast H _ y)).
\ No newline at end of file
+  intros. Fail refine (Cons (cast H _ y)).
+  Unset Solve Unification Constraints. (* Keep the unification constraint around *)
+  refine (Cons (cast H _ y)).
+  intros.
+  refine (Nest (prod X X)). Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index 495e67e09..f5a22bd50 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -650,4 +650,5 @@ Goal    forall (ptest : program) (cond : Condition) (value : bool)
 
   Grab Existential Variables.
   subst_body; simpl.
-  refine (all_behead (projT2 _)).
+  Fail refine (all_behead (projT2 _)).
+  Unset Solve Unification Constraints. refine (all_behead (projT2 _)).
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
index b97a8ce64..3189685ec 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,3 +1,4 @@
 Goal exists x, x.
+Unset Solve Unification Constraints.
 unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
 (* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
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
diff --git a/test-suite/bugs/closed/5149.v b/test-suite/bugs/closed/5149.v
new file mode 100644
index 000000000..684dba196
--- /dev/null
+++ b/test-suite/bugs/closed/5149.v
@@ -0,0 +1,47 @@
+Goal forall x x' : nat, x = x' -> S x = S x -> exists y, S y = S x.
+intros.
+eexists.
+rewrite <- H.
+eassumption.
+Qed.
+
+Goal forall (base_type_code : Type) (t : base_type_code) (flat_type : Type) 
+            (t' : flat_type) (exprf interp_flat_type0 interp_flat_type1 : 
+flat_type -> Type)
+            (v v' : interp_flat_type1 t'),
+    v = v' ->
+    forall (interpf : forall t0 : flat_type, exprf t0 -> interp_flat_type1 t0)
+           (SmartVarVar : forall t0 : flat_type, interp_flat_type1 t0 -> 
+interp_flat_type0 t0)
+           (Tbase : base_type_code -> flat_type) (x : exprf (Tbase t))
+           (x' : interp_flat_type1 (Tbase t)) (T : Type)
+           (flatten_binding_list : forall t0 : flat_type,
+               interp_flat_type0 t0 -> interp_flat_type1 t0 -> list T)
+           (P : T -> list T -> Prop) (prod : Type -> Type -> Type)
+           (s : forall x0 : base_type_code, prod (exprf (Tbase x0)) 
+(interp_flat_type1 (Tbase x0)) -> T)
+           (pair : forall A B : Type, A -> B -> prod A B),
+      P (s t (pair (exprf (Tbase t)) (interp_flat_type1 (Tbase t)) x x'))
+        (flatten_binding_list t' (SmartVarVar t' v') v) ->
+      (forall (t0 : base_type_code) (t'0 : flat_type) (v0 : interp_flat_type1 
+t'0)
+              (x0 : exprf (Tbase t0)) (x'0 : interp_flat_type1 (Tbase t0)),
+          P (s t0 (pair (exprf (Tbase t0)) (interp_flat_type1 (Tbase t0)) x0 
+x'0))
+            (flatten_binding_list t'0 (SmartVarVar t'0 v0) v0) -> interpf 
+(Tbase t0) x0 = x'0) ->
+      interpf (Tbase t) x = x'.
+Proof.
+  intros ?????????????????????? interpf_SmartVarVar.
+  solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail 
+"too early".
+  Undo.
+  (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *)
+  Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
+  solve [eapply interpf_SmartVarVar; subst; eassumption].
+  Undo.
+  Unset Solve Unification Constraints.
+  (* User control of when constraints are solved *)
+  solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ].
+Qed.
+
diff --git a/test-suite/bugs/closed/HoTT_coq_117.v b/test-suite/bugs/closed/HoTT_coq_117.v
index 5fbcfef4e..de60fd0ae 100644
--- a/test-suite/bugs/closed/HoTT_coq_117.v
+++ b/test-suite/bugs/closed/HoTT_coq_117.v
@@ -16,10 +16,29 @@ Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A,
 Admitted.
 
 Inductive Empty : Set := .
-Instance contr_from_Empty {_ : Funext} (A : Type) :
+Fail Instance contr_from_Empty {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect _ x)).
+
+Fail Instance contr_from_Empty {F : Funext} (A : Type) :
   Contr_internal (Empty -> A) :=
   BuildContr _
              (Empty_rect (fun _ => A))
              (fun f => path_forall _ f (fun x => Empty_rect _ x)).
+
+(** This could be disallowed, this uses the Funext argument *)
+Instance contr_from_Empty {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)).
+
+Instance contr_from_Empty' {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)).
 (* Toplevel input, characters 15-220:
 Anomaly: unknown meta ?190. Please report. *)
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c76fc74a0..b9413a4ac 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,4 +1,5 @@
 (* Set Printing Existential Instances. *)
+Unset Solve Unification Constraints.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
 Goal True /\ True /\ True \/
              veeryyyyyyyyyyyyloooooooooooooonggidentifier =
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 1bc6fee0c..64ba6b1e3 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -31,3 +31,6 @@ Global Set Refolding Reduction.
 Global Set Typeclasses Legacy Resolution.
 Global Set Typeclasses Limit Intros.
 Global Unset Typeclasses Filtered Unification.
+
+(** Allow silently letting unification constraints float after a "." *)
+Global Unset Solve Unification Constraints.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 12c387dcf..7ffe680e5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1129,7 +1129,7 @@ let interp_recursive isfix fixl notations =
       () in
 
   (* Instantiate evars and check all are resolved *)
-  let evd = consider_remaining_unif_problems env_rec !evdref in
+  let evd = solve_unif_constraints_with_heuristics env_rec !evdref in
   let evd, nf = nf_evars_and_universes evd in
   let fixdefs = List.map (Option.map nf) fixdefs in
   let fixtypes = List.map nf fixtypes in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8a28d979c..68485231b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1573,7 +1573,7 @@ let get_current_context_of_args = function
 let vernac_check_may_eval redexp glopt rc =
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma', c = interp_open_constr env sigma rc in
-  let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
+  let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
   let pl, uctx = Evd.universe_context sigma' in