From 7efeff178470ab204e531cd07176091bf5022da6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 20 Oct 2014 12:56:43 +0200 Subject: A patch for printing "match" when constructors are defined with let-in but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there. --- pretyping/detyping.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping/detyping.mli') diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index b2fc92557..8a8312990 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -34,10 +34,10 @@ val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob val detype_case : bool -> ('a -> glob_constr) -> - (constructor array -> int array -> 'a array -> + (constructor array -> bool list array -> 'a array -> (Loc.t * Id.t list * cases_pattern list * glob_constr) list) -> - ('a -> int -> bool) -> - Id.t list -> inductive * case_style * int array * int -> + ('a -> bool list -> bool) -> + Id.t list -> inductive * case_style * bool list array * bool list -> 'a option -> 'a -> 'a array -> glob_constr val detype_sort : sorts -> glob_sort @@ -55,11 +55,11 @@ val synthetize_type : unit -> bool (** Utilities to transform kernel cases to simple pattern-matching problem *) -val it_destRLambda_or_LetIn_names : int -> glob_constr -> Name.t list * glob_constr +val it_destRLambda_or_LetIn_names : bool list -> glob_constr -> Name.t list * glob_constr val simple_cases_matrix_of_branches : - inductive -> (int * int * glob_constr) list -> cases_clauses + inductive -> (int * bool list * glob_constr) list -> cases_clauses val return_type_of_predicate : - inductive -> int -> glob_constr -> predicate_pattern * glob_constr option + inductive -> bool list -> glob_constr -> predicate_pattern * glob_constr option val subst_genarg_hook : (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t -- cgit v1.2.3