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. --- kernel/term.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index 50cd433e9..c5e85b1e5 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -47,7 +47,7 @@ type case_style = Constr.case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle type case_printing = Constr.case_printing = - { ind_nargs : int; style : case_style } + { ind_tags : bool list; cstr_tags : bool list array; style : case_style } type case_info = Constr.case_info = { ci_ind : inductive; -- cgit v1.2.3