Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed

to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body)
instead of looking it up in the environment. A version of the same functions
with the old type is put in Inductiveops (outside the kernel).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 8 insertions, 8 deletions

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 15d10e84c9..9dce63191f 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -129,7 +129,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
     try destApplication intype with 
 	Invalid_argument _ -> (intype,[||])  in
   let ind=destInd h in 
-  let types=Inductive.arities_of_constructors env ind in
+  let types=Inductiveops.arities_of_constructors env ind in
   let lp=Array.length types in
   let ci=(snd cstr)-1 in
   let branch i=
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 8b5c30521e..9dbda969a1 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -48,13 +48,13 @@ let rec nb_prod_after n c=
 let construct_nhyps ind gls =
   let env=pf_env gls in
   let nparams = (snd (Global.lookup_inductive ind)).mind_nparams in
-  let constr_types = Inductive.arities_of_constructors (pf_env gls) ind in 
+  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in 
   let hyp = nb_prod_after nparams in	
     Array.map hyp constr_types
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
 let ind_hyps nevar ind largs gls= 
-  let types= Inductive.arities_of_constructors (pf_env gls) ind in 
+  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in 
   let lp=Array.length types in     
   let myhyps i=
     let t1=Term.prod_applist types.(i) largs in
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index dca5963f9a..10a428e832 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -243,9 +243,9 @@ let typeur sigma metamap =
         let cb = Environ.lookup_constant c env in
         T.body_of_type cb.Declarations.const_type
     | T.Evar ev -> Evd.existential_type sigma ev
-    | T.Ind ind -> T.body_of_type (Inductive.type_of_inductive env ind)
+    | T.Ind ind -> T.body_of_type (Inductiveops.type_of_inductive env ind)
     | T.Construct cstr ->
-       T.body_of_type (Inductive.type_of_constructor env cstr)
+       T.body_of_type (Inductiveops.type_of_constructor env cstr)
     | T.Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 728c7ac9a7..d4093f002c 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -124,10 +124,10 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         E.make_judge cstr (E.constant_type env c)
 	  
      | T.Ind ind ->
-        E.make_judge cstr (Inductive.type_of_inductive env ind)
+        E.make_judge cstr (Inductiveops.type_of_inductive env ind)
 	  
      | T.Construct cstruct -> 
-        E.make_judge cstr (Inductive.type_of_constructor env cstruct)
+        E.make_judge cstr (Inductiveops.type_of_constructor env cstruct)
 	  
      | T.Case (ci,p,c,lf) ->
         let expectedtype =
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index f448dd4ed1..41967dede6 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -406,7 +406,7 @@ let mk_inductive_obj sp packs variables hyps finite =
             D.mind_typename=typename ;
             D.mind_nf_arity=arity} = p
        in
-        let lc = Inductive.arities_of_constructors (Global.env ()) (sp,!tyno) in
+        let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in
         let cons =
          (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
           (Array.mapi