diff options
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 37eaa58026..cc781c8712 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -66,3 +66,12 @@ val w_merge : env -> bool -> unify_flags -> evar_map * (metavariable * constr * (instance_constraint * instance_typing_status)) list * (env * types pexistential * types) list -> evar_map +val unify_0 : Environ.env -> + Evd.evar_map -> + Evd.conv_pb -> + unify_flags -> + Term.types -> + Term.types -> + Evd.evar_map * Evd.metabinding list * + (Environ.env * Term.types Term.pexistential * Term.constr) list + |