Merge commit 'e6edb33' into v8.6

Was PR#331: Solve_constraints and Set Use Unification Heuristics

4 files changed, 33 insertions, 1 deletions

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 a3ece19134..eddbf72a89 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 e5114a2eca..3f55270609 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 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. *)