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 +++++-
 test-suite/bugs/closed/4763.v         | 13 +++++++++++++
 test-suite/bugs/closed/HoTT_coq_117.v | 21 ++++++++++++++++++++-
 3 files changed, 38 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/4763.v

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]
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
new file mode 100644
index 0000000000..ae8ed0e6e8
--- /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/HoTT_coq_117.v b/test-suite/bugs/closed/HoTT_coq_117.v
index 5fbcfef4e0..de60fd0ae4 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. *)
-- 
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.
---
 engine/proofview.ml                 |  4 ----
 engine/proofview.mli                |  1 -
 ltac/extratactics.ml4               |  5 ++++
 pretyping/unification.ml            | 19 ++++-----------
 proofs/pfedit.ml                    | 16 +++++++++++++
 proofs/refine.ml                    | 11 +++++++++
 proofs/refine.mli                   |  5 ++++
 test-suite/bugs/closed/2310.v       |  6 ++++-
 test-suite/bugs/closed/3647.v       |  3 ++-
 test-suite/bugs/closed/4416.v       |  1 +
 test-suite/bugs/closed/5149.v       | 47 +++++++++++++++++++++++++++++++++++++
 test-suite/output/unifconstraints.v |  1 +
 12 files changed, 98 insertions(+), 21 deletions(-)
 create mode 100644 test-suite/bugs/closed/5149.v

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 855235d2b0..c01879765b 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 725445251d..90be2f90ab 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 d0318fb5f6..e6498e02b2 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -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/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
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a3ece19134..9c71e107cc 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 = "Unification heuristics are applied at every .";
+  Goptions.optkey = ["Use";"Unification";"Heuristics"];
+  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 e5114a2eca..2f21428900 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.consider_remaining_unif_problems env sigma in
+       Unsafe.tclEVARSADVANCE sigma
+   with e -> tclZERO e
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 3d140f036b..a44632eff5 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/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v
index 0be859eddf..9fddede7e9 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 Use Unification Heuristics. (* 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 495e67e09e..f2cd41203c 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 Use Unification Heuristics. refine (all_behead (projT2 _)).
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
index b97a8ce640..afe8c62ed0 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,3 +1,4 @@
 Goal exists x, x.
+Unset Use Unification Heuristics.
 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/5149.v b/test-suite/bugs/closed/5149.v
new file mode 100644
index 0000000000..01b9d158fe
--- /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 Use Unification Heuristics.
+  (* User control of when constraints are solved *)
+  solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ].
+Qed.
+
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c76fc74a0c..c7fb82adac 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,4 +1,5 @@
 (* Set Printing Existential Instances. *)
+Unset Use Unification Heuristics.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
 Goal True /\ True /\ True \/
              veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-- 
cgit v1.2.3


From c9f8f7fe182decedda2e6403d502fda3aff24a6e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 22 Oct 2016 10:37:17 +0200
Subject: Add Unset Use Unif Heuristics in Compat/Coq85

---
 theories/Compat/Coq85.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 4007536442..ba58e2d88b 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -27,3 +27,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 Use Unification Heuristics.
\ No newline at end of file
-- 
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
---
 plugins/ssrmatching/ssrmatching.ml4 | 2 +-
 plugins/ssrmatching/ssrmatching.mli | 2 +-
 pretyping/evarconv.ml               | 8 +++++---
 pretyping/evarconv.mli              | 3 +++
 pretyping/evarsolve.ml              | 6 ++++--
 pretyping/evarsolve.mli             | 3 +++
 pretyping/pretyping.ml              | 2 +-
 pretyping/unification.ml            | 6 +++---
 proofs/refine.ml                    | 2 +-
 tactics/class_tactics.ml            | 2 +-
 tactics/equality.ml                 | 3 ++-
 toplevel/command.ml                 | 2 +-
 toplevel/vernacentries.ml           | 2 +-
 13 files changed, 27 insertions(+), 16 deletions(-)

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index a34fa4cae7..88f028b4b7 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -355,7 +355,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 74a603e51c..288a04e60a 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 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
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 2f21428900..3f55270609 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -157,6 +157,6 @@ end }
 let solve_constraints =
   let open Proofview in
   tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
-   try let sigma = Evarconv.consider_remaining_unif_problems env sigma in
+   try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
        Unsafe.tclEVARSADVANCE sigma
    with e -> tclZERO e
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 0944cbe38f..9ea4027263 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1437,7 +1437,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 e9d08d7375..bb3cbad92b 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/toplevel/command.ml b/toplevel/command.ml
index 12c387dcf3..7ffe680e5e 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 f69bac437e..9d3837d2e2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1497,7 +1497,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
-- 
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.

---
 ltac/extratactics.ml4               |  4 ++--
 ltac/g_auto.ml4                     |  2 +-
 ltac/tacinterp.ml                   |  8 ++++----
 pretyping/pretyping.ml              | 10 +++++-----
 pretyping/pretyping.mli             |  2 +-
 proofs/evar_refiner.ml              |  2 +-
 proofs/pfedit.ml                    |  4 ++--
 tactics/tactics.ml                  |  2 +-
 test-suite/bugs/closed/2310.v       |  2 +-
 test-suite/bugs/closed/3647.v       |  2 +-
 test-suite/bugs/closed/4416.v       |  2 +-
 test-suite/bugs/closed/5149.v       |  2 +-
 test-suite/output/unifconstraints.v |  2 +-
 theories/Compat/Coq85.v             |  2 +-
 14 files changed, 23 insertions(+), 23 deletions(-)

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index e6498e02b2..2cca760c38 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 }
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 8bc2ffd654..22a2d7fc2f 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 08e67a0c2f..b9dcc4e18d 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/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
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 5f0cc73d2c..29cad06352 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 9c71e107cc..eddbf72a89 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -16,8 +16,8 @@ open Evd
 let use_unification_heuristics_ref = ref true
 let _ = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
-  Goptions.optname = "Unification heuristics are applied at every .";
-  Goptions.optkey = ["Use";"Unification";"Heuristics"];
+  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);
 }
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 893f33f1a8..e8cf09415c 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 9fddede7e9..7fae328715 100644
--- a/test-suite/bugs/closed/2310.v
+++ b/test-suite/bugs/closed/2310.v
@@ -15,7 +15,7 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
    leave P as subgoal or choose itself one solution *)
 
   intros. Fail refine (Cons (cast H _ y)).
-  Unset Use Unification Heuristics. (* Keep the unification constraint around *)
+  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 f2cd41203c..f5a22bd508 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -651,4 +651,4 @@ Goal    forall (ptest : program) (cond : Condition) (value : bool)
   Grab Existential Variables.
   subst_body; simpl.
   Fail refine (all_behead (projT2 _)).
-  Unset Use Unification Heuristics. 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 afe8c62ed0..3189685ec0 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,4 +1,4 @@
 Goal exists x, x.
-Unset Use Unification Heuristics.
+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/5149.v b/test-suite/bugs/closed/5149.v
index 01b9d158fe..684dba1961 100644
--- a/test-suite/bugs/closed/5149.v
+++ b/test-suite/bugs/closed/5149.v
@@ -40,7 +40,7 @@ Proof.
   Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
   solve [eapply interpf_SmartVarVar; subst; eassumption].
   Undo.
-  Unset Use Unification Heuristics.
+  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/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c7fb82adac..b9413a4ac2 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,5 +1,5 @@
 (* Set Printing Existential Instances. *)
-Unset Use Unification Heuristics.
+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 ba58e2d88b..c644133839 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -29,4 +29,4 @@ Global Set Typeclasses Limit Intros.
 Global Unset Typeclasses Filtered Unification.
 
 (** Allow silently letting unification constraints float after a "." *)
-Global Unset Use Unification Heuristics.
\ No newline at end of file
+Global Unset Solve Unification Constraints.
-- 
cgit v1.2.3