diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index ea0f063fe4..77985c8d73 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -29,18 +29,18 @@ val new_untyped_evar : unit -> existential_key (** {6 Creating a fresh evar given their type and context} *) val new_evar : - evar_map -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> + evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> types -> evar_map * constr (** the same with side-effects *) val e_new_evar : - evar_map ref -> env -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> + evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - ?src:loc * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr + ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -49,7 +49,7 @@ val new_type_evar : of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:loc * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr + named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (identifier * constr) list @@ -158,7 +158,7 @@ val empty_valcon : val_constraint val mk_valcon : constr -> val_constraint val split_tycon : - loc -> env -> evar_map -> type_constraint -> + Loc.t -> env -> evar_map -> type_constraint -> evar_map * (name * type_constraint * type_constraint) val valcon_of_tycon : type_constraint -> val_constraint |