diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-20 12:56:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-20 23:29:19 +0200 |
| commit | 7efeff178470ab204e531cd07176091bf5022da6 (patch) | |
| tree | afdc79d6eb2a371fa2cec235aabea3c5425d46b9 /pretyping/detyping.mli | |
| parent | f00f8482e1d21ef8b03044ed2162cb29d9e4537d (diff) | |
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.
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 12 |
1 files changed, 6 insertions, 6 deletions
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 |