diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/cic.mli | 3 |
1 files changed, 2 insertions, 1 deletions
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 *) |