diff options
Diffstat (limited to 'proofs/refine.mli')
-rw-r--r-- | proofs/refine.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/proofs/refine.mli b/proofs/refine.mli index 205b97974..1a254d578 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 -> EConstr.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. *) |