diff options
| author | Pierre-Marie Pédrot | 2021-01-04 10:52:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-12 13:20:29 +0100 |
| commit | 71b5649acf83acb3fe6f1c5ddc468d5c504b7983 (patch) | |
| tree | 1c8bf4e04fbd91e30d613819ca39522cc8302715 /pretyping/pattern.ml | |
| parent | bedea3079b35982abefe4b78ae7aa0f6819842f6 (diff) | |
Change the case representation of patterns.
Diffstat (limited to 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index f6d61f4892..553511f1bf 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -18,7 +18,6 @@ type patvar = Id.t type case_info_pattern = { cip_style : Constr.case_style; cip_ind : inductive option; - cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) cip_extensible : bool (** does this match end with _ => _ ? *) } type constr_pattern = @@ -35,8 +34,8 @@ type constr_pattern = | PSort of Sorts.family | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern - | PCase of case_info_pattern * constr_pattern * constr_pattern * - (int * bool list * constr_pattern) list (** index of constructor, nb of args *) + | PCase of case_info_pattern * (Name.t array * constr_pattern) option * constr_pattern * + (int * Name.t array * constr_pattern) list (** index of constructor, nb of args *) | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) | PInt of Uint63.t |