diff options
| author | coqbot-app[bot] | 2021-01-18 13:04:52 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-18 13:04:52 +0000 |
| commit | 4efb4b01c6f44127c6c0982ee777651de2ab9204 (patch) | |
| tree | a6007ad7398525ca93d21766d481f65ff5e19763 /pretyping/pattern.ml | |
| parent | 5b08cdcd4bde7fdcd21f7a0f0912f0021847294b (diff) | |
| parent | 4c67572a623e0caf24839e9e6af76bdc6bdf1ac0 (diff) | |
Merge PR #13723: Use a compact case representation for patterns
Reviewed-by: mattam82
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 |