From c5ecebf6fefbaa673dda506175a2aa4a69d79807 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Sep 2014 00:03:46 +0200 Subject: 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. --- pretyping/detyping.mli | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'pretyping/detyping.mli') 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 *) -- cgit v1.2.3