1 files changed, 11 insertions, 0 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml
index c36bb143e..1ee6e0ca5 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -152,3 +152,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