From 8f4b002c44c4820131acd929d31502ab7cf952c4 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 14 Jun 2010 09:29:47 +0000 Subject: 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 --- kernel/inductive.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/inductive.mli') 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: -- cgit v1.2.3