diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 00:03:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 00:10:03 +0200 |
| commit | c5ecebf6fefbaa673dda506175a2aa4a69d79807 (patch) | |
| tree | e364fd928f247c249767ffb679b0265857327a6a /pretyping/detyping.mli | |
| parent | 4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (diff) | |
Revert specific syntax for primitive projections, avoiding ugly
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
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 *) |