From dce9fe9bd4cab3e560f41a8d7cbf447b27665e1f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 13 Sep 2009 13:24:21 +0000
Subject: - Inductive types in the "using" option of auto/eauto/firstorder are 
  interpreted as using the collection of their constructors as hints. - Add
 support for both "using" and "with" in "firstorder". Made the   syntax of
 "using" compatible with the one of "auto" by separating   lemmas by commas.
 Did not fully merge the syntax: auto accepts   constr while firstorder
 accepts names (but are constr really useful?). - Added "Reserved Infix" as a
 specific shortcut of the corresponding   "Reserved Notation".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/inductiveops.ml  | 5 ++++-
 pretyping/inductiveops.mli | 2 ++
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3150ed63b5..727fd6f859 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -71,7 +71,6 @@ let substnl_ind_type l n = map_inductive_type (substnl l n)
 let mkAppliedInd (IndType ((ind,params), realargs)) =
   applist (mkInd ind,params@realargs)
 
-
 (* Does not consider imbricated or mutually recursive types *) 
 let mis_is_recursive_subset listind rarg = 
   let rec one_is_rec rvec = 
@@ -125,6 +124,10 @@ let get_full_arity_sign env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_arity_ctxt
 
+let nconstructors ind = 
+  let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+  Array.length mip.mind_consnames
+
 (* Length of arity (w/o local defs) *)
 
 let inductive_nargs env ind =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index cc1bb7f418..cea769955e 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -58,6 +58,8 @@ val mis_nf_constructor_type :
 val mis_constr_nargs : inductive -> int array
 val mis_constr_nargs_env : env -> inductive -> int array
 
+val nconstructors : inductive -> int
+
 (* Return the lengths of parameters signature and real arguments signature *)
 val inductive_nargs : env -> inductive -> int * int
 
-- 
cgit v1.2.3