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.
---
 checker/cic.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/cic.mli b/checker/cic.mli
index 1313208a3a..f00c957058 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -53,7 +53,8 @@ type metavariable = int
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle
   | RegularStyle (** infer printing form from number of constructor *)
 type case_printing =
-  { ind_nargs : int; (** length of the arity of the inductive type *)
+  { ind_tags : bool list; (* tell whether letin or lambda in the arity of the inductive type *)
+    cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *)
     style     : case_style }
 
 (** the integer is the number of real args, needed for reduction *)
-- 
cgit v1.2.3