Merge branch 'v8.6'

1 files changed, 11 insertions, 0 deletions

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