aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching/ssrmatching.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssrmatching/ssrmatching.mli')
-rw-r--r--plugins/ssrmatching/ssrmatching.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index fa0c2f5b1..894cdb943 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -213,7 +213,7 @@ val assert_done : 'a option ref -> 'a
(** Very low level APIs.
these are calls to evarconv's [the_conv_x] followed by
- [consider_remaining_unif_problems] and [resolve_typeclasses].
+ [solve_unif_constraints_with_heuristics] and [resolve_typeclasses].
In case of failure they raise [NoMatch] *)
val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map