From 7efeff178470ab204e531cd07176091bf5022da6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Oct 2014 12:56:43 +0200
Subject: 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.
---
 intf/pattern.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'intf/pattern.mli')

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