diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-14 09:29:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-14 09:29:47 +0000 |
| commit | 8f4b002c44c4820131acd929d31502ab7cf952c4 (patch) | |
| tree | 652c63b712b5d2784adde12d9849527673f98de8 /kernel/inductive.mli | |
| parent | 2c9c92aac97160a40ff240dec41464ae78a6c88c (diff) | |
Added printing of recursive notations in cases pattern (supported by wish 2248).
Note that the code is no longer in constrextern.ml but in topconstr.ml where
the code for reversing notations of term already was.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13132 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 73bd2692e..42a2da41b 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -50,6 +50,7 @@ val type_of_constructors : inductive -> mind_specif -> types array (** Transforms inductive specification into types (in nf) *) val arities_of_specif : mutual_inductive -> mind_specif -> types array +val inductive_params : mind_specif -> int (** [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: |