Merge branch 'v8.6'

6 files changed, 45 insertions, 1 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index ff0df9179f..509efbc5b8 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 c7f5efd5aa..80bea0c3b1 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 d4920e5051..c238f731d5 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -151,3 +151,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. *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index e41fb94cce..030a3cbfb9 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -173,6 +173,9 @@ module New = struct
   let pf_unsafe_type_of gl t =
     pf_apply unsafe_type_of gl t
 
+  let pf_get_type_of gl t =
+    pf_apply (Retyping.get_type_of ~lax:true) gl t
+
   let pf_type_of gl t =
     pf_apply type_of gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 727efcf6dc..59f296f64e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -108,7 +108,16 @@ module New : sig
   val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
   val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
 
+  (** WRONG: To be avoided at all costs, it typechecks the term entirely but
+     forgets the universe constraints necessary to retypecheck it *)
   val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+
+  (** This function does no type inference and expects an already well-typed term.
+      It recomputes its type in the fastest way possible (no conversion is ever involved) *)
+  val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+
+  (** This function entirely type-checks the term and computes its type
+      and the implied universe constraints. *)
   val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
   val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool