diff options
Diffstat (limited to 'pretyping/detyping.mli')
-rw-r--r-- | pretyping/detyping.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 8a8302b8b..b2fc92557 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -28,8 +28,9 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr [isgoal] tells if naming must avoid global-level synonyms as intro does [ctx] gives the names of the free variables *) -val detype : bool -> Id.t list -> names_context -> - evar_map -> constr -> glob_constr +val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr + +val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr val detype_case : bool -> ('a -> glob_constr) -> @@ -41,7 +42,7 @@ val detype_case : val detype_sort : sorts -> glob_sort -val detype_rel_context : constr option -> Id.t list -> names_context -> +val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> evar_map -> rel_context -> glob_decl list (** look for the index of a named var or a nondep var as it is renamed *) |