diff options
| author | Hugo Herbelin | 2014-10-20 12:56:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-20 23:29:19 +0200 |
| commit | 7efeff178470ab204e531cd07176091bf5022da6 (patch) | |
| tree | afdc79d6eb2a371fa2cec235aabea3c5425d46b9 /intf/pattern.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 'intf/pattern.mli')
| -rw-r--r-- | intf/pattern.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/intf/pattern.mli b/intf/pattern.mli index 4fa5f418d0..b04db3bfae 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -55,7 +55,7 @@ type extended_patvar_map = constr_under_binders Id.Map.t type case_info_pattern = { cip_style : case_style; cip_ind : inductive option; - cip_ind_args : int option; (** number of params and args *) + cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) cip_extensible : bool (** does this match end with _ => _ ? *) } type constr_pattern = @@ -73,7 +73,7 @@ type constr_pattern = | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of case_info_pattern * constr_pattern * constr_pattern * - (int * int * constr_pattern) list (** index of constructor, nb of args *) + (int * bool list * constr_pattern) list (** index of constructor, nb of args *) | PFix of fixpoint | PCoFix of cofixpoint |