diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index c03374c59f..c4f0f18e27 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -148,7 +148,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> Ev type pretyper = { pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun; pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun; - pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun; + pretype_evar : pretyper -> existential_name * (lident * glob_constr) list -> unsafe_judgment pretype_fun; pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun; pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun; pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun; |