- 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

2 files changed, 6 insertions, 1 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3150ed63b..727fd6f85 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 cc1bb7f41..cea769955 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