diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 18e416596e..ee57f690a1 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -38,7 +38,11 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> val search_guard : ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +type typing_constraint = + | UnknownIfTermOrType (** E.g., unknown if manual implicit arguments allowed *) + | IsType (** Necessarily a type *) + | OfType of types (** A term of the expected type *) + | WithoutTypeConstraint (** A term of unknown expected type *) type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr |