diff options
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 9156623f5..1b8f9ccd8 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -35,6 +35,11 @@ val w_unify_to_subterm : val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs +(* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type + [ctyp] so that its gets type [typ]; [typ] may contain metavariables *) +val w_coerce_to_type : env -> evar_defs -> constr -> types -> types -> + evar_defs * constr + (*i This should be in another module i*) (* [abstract_list_all env evd t c l] *) |