9 files changed, 64 insertions, 2 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/proof.ml b/proofs/proof.ml
index 0a3b08c04a..b2103489a7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -372,6 +372,22 @@ let in_proof p k = k (Proofview.return p.proofview)
 let unshelve p =
   { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] }
 
+let pr_proof p =
+  let p = map_structured_proof p (fun _sigma g -> g) in
+  Pp.(
+    let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
+    let rec aux acc = function
+      | [] -> acc
+      | (before,after)::stack ->
+         aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++
+              pr_goal_list after) stack in
+    str "[" ++ str "focus structure: " ++
+               aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++
+    str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++
+    str "given up: " ++ pr_goal_list p.given_up_goals ++
+    str "]"
+  )
+
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
   let subgoals p =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 5053fc7fb9..8dc165e72e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -182,6 +182,8 @@ val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
    focused goals. *)
 val unshelve : proof -> proof
 
+val pr_proof : proof -> Pp.std_ppcmds
+
 (*** Compatibility layer with <=v8.2 ***)
 module V82 : sig
   val subgoals : proof -> Goal.goal list Evd.sigma
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2956d623fd..a2ee622215 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -622,7 +622,7 @@ module Bullet = struct
     let _ = register_behavior strict
   end
 
-  (* Current bullet behavior, controled by the option *)
+  (* Current bullet behavior, controlled by the option *)
   let current_behavior = ref Strict.strict
 
   let _ =
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