aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/constr.mli')
-rw-r--r--kernel/constr.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli
index da7ac6a0d..1e23911dd 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -26,7 +26,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; (** tell whether letin or lambda in the signature of each constructor *)
style : case_style }
(** the integer is the number of real args, needed for reduction *)