diff options
| author | Matthieu Sozeau | 2018-08-15 14:22:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:14:10 +0100 |
| commit | 2cf15ef8e3ddebe285ec0e9f5f8715b025ba4eec (patch) | |
| tree | 4d4e075161b3d54e7fd49ed90d830f2e478aac6e /pretyping/evarconv.mli | |
| parent | af9b88c253b578ad53ee884ff3102d0a74056a1e (diff) | |
Rename types_or_terms and the unification function types
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index c2ad4e6678..bd55b952a6 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -24,7 +24,7 @@ val default_flags_of : ?subterm_ts:transparent_state -> transparent_state -> uni type unify_fun = unify_flags -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result -val conv_fun : unify_fun -> unify_flags -> Evarsolve.conv_fun +val conv_fun : unify_fun -> unify_flags -> Evarsolve.unifier exception UnableToUnify of evar_map * Pretype_errors.unification_error |