aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/detyping.mli')
-rw-r--r--pretyping/detyping.mli7
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 *)