From 71b5649acf83acb3fe6f1c5ddc468d5c504b7983 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Jan 2021 10:52:38 +0100
Subject: Change the case representation of patterns.

---
 pretyping/pattern.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'pretyping/pattern.ml')

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
-- 
cgit v1.2.3