diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-11 15:15:46 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-11 15:15:46 +0000 |
| commit | a07e31a2693bde01d3dca59364693096d550561a (patch) | |
| tree | 322e0acb77a7dfc1a2276b88a73357ffc09a08a7 /kernel/term.mli | |
| parent | 9cfe880e1f5f9dddd63aa269a2fb159665c2d182 (diff) | |
Ensures that let-in's in arities of inductive types work well. Maybe not
very useful in practice but as soon as let-in's were not forbidden in
the internal data structure, better to do it. Moreover, this gets
closer to the view were inductive definitions are uniformly built from
"contexts". (checker not changed!)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 8f45e39f0..bc1cac44a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -42,7 +42,7 @@ type metavariable = int (*s Case annotation *) type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle type case_printing = - { ind_nargs : int; (* number of real args of the inductive type *) + { ind_nargs : int; (* length of the arity of the inductive type *) style : case_style } (* the integer is the number of real args, needed for reduction *) type case_info = |