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

16 files changed, 67 insertions, 29 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
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5f9f907f52..5aee04f7d7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -317,9 +317,10 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
 
 let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
   let auxntyp = 1 in
+  let specif = lookup_mind_specif env mi in
   let env' =
     push_rel (Anonymous,None,
-              hnf_prod_applist env (type_of_inductive env mi) lpar) env in
+              hnf_prod_applist env (type_of_inductive specif) lpar) env in
   let ra_env' = 
     (Imbr mi,Rtree.mk_param 0) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 545b5b83a1..ab2177f75c 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -18,6 +18,8 @@ open Environ
 open Reduction
 open Type_errors
 
+type mind_specif = mutual_inductive_body * one_inductive_body
+
 (* raise Not_found if not an inductive type *)
 let lookup_mind_specif env (kn,tyi) =
   let mib = Environ.lookup_mind kn env in
@@ -93,16 +95,13 @@ let full_constructor_instantiate (((mind,_),mib,mip),params) =
 
 (* Type of an inductive type *)
 
-let type_of_inductive env i =
-  let (_,mip) = lookup_mind_specif env i in
-  mip.mind_user_arity
+let type_of_inductive (_,mip) = mip.mind_user_arity
 
 (************************************************************************)
 (* Type of a constructor *)
 
-let type_of_constructor env cstr =
+let type_of_constructor cstr (mib,mip) =
   let ind = inductive_of_constructor cstr in
-  let (mib,mip) = lookup_mind_specif env ind in
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
@@ -113,8 +112,8 @@ let arities_of_specif kn (mib,mip) =
   let specif = mip.mind_nf_lc in
   Array.map (constructor_instantiate kn mib) specif
 
-let arities_of_constructors env ind = 
-  arities_of_specif (fst ind) (lookup_mind_specif env ind)
+let arities_of_constructors ind specif = 
+  arities_of_specif (fst ind) specif
 
 
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 0ecfe2a8c4..0174b80201 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -28,24 +28,24 @@ val find_rectype     : env -> types -> inductive * constr list
 val find_inductive   : env -> types -> inductive * constr list
 val find_coinductive : env -> types -> inductive * constr list
 
+type mind_specif = mutual_inductive_body * one_inductive_body
+
 (*s Fetching information in the environment about an inductive type.
     Raises [Not_found] if the inductive type is not found. *)
-val lookup_mind_specif :
-  env -> inductive -> mutual_inductive_body * one_inductive_body
+val lookup_mind_specif : env -> inductive -> mind_specif
 
 (*s Functions to build standard types related to inductive *)
 
-val type_of_inductive    : env -> inductive -> types
+val type_of_inductive : mind_specif -> types
 
 (* Return type as quoted by the user *)
-val type_of_constructor  : env -> constructor -> types
+val type_of_constructor : constructor -> mind_specif -> types
 
 (* Return constructor types in normal form *)
-val arities_of_constructors : env -> inductive -> types array
+val arities_of_constructors : inductive -> mind_specif -> types array
 
 (* Transforms inductive specification into types (in nf) *)
-val arities_of_specif : mutual_inductive -> 
-  mutual_inductive_body * one_inductive_body -> types array 
+val arities_of_specif : mutual_inductive -> mind_specif -> types array 
 
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 05b7619e52..1a3dd19f88 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,7 +252,8 @@ let judge_of_inductive env i =
     let (kn,_) = i in
     let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
-  make_judge constr (type_of_inductive env i)
+  let specif = lookup_mind_specif env i in
+  make_judge constr (type_of_inductive specif)
 
 (*
 let toikey = Profile.declare_profile "judge_of_inductive";;
@@ -268,7 +269,8 @@ let judge_of_constructor env c =
     let ((kn,_),_) = c in
     let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
-  make_judge constr (type_of_constructor env c)
+  let specif = lookup_mind_specif env (inductive_of_constructor c) in
+  make_judge constr (type_of_constructor c specif)
 
 (*
 let tockey = Profile.declare_profile "judge_of_constructor";;
diff --git a/library/global.ml b/library/global.ml
index 9ad01842cb..6606200866 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -134,7 +134,12 @@ open Libnames
 let type_of_reference env = function
   | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t
   | ConstRef c -> Environ.constant_type env c
-  | IndRef ind -> Inductive.type_of_inductive env ind
-  | ConstructRef cstr -> Inductive.type_of_constructor env cstr
+  | IndRef ind ->
+     let specif = Inductive.lookup_mind_specif env ind in
+      Inductive.type_of_inductive specif
+  | ConstructRef cstr ->
+     let specif =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+       Inductive.type_of_constructor cstr specif
 
 let type_of_global t = type_of_reference (env ()) t
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 7df78fe61c..bbbbc31800 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -507,7 +507,7 @@ let print_opaque_name qid =
     | IndRef (sp,_) ->
         print_mutual sp
     | ConstructRef cstr -> 
-	let ty = Inductive.type_of_constructor env cstr in
+	let ty = Inductiveops.type_of_constructor env cstr in
 	print_typed_value (mkConstruct cstr, ty)
     | VarRef id ->
         let (_,c,ty) = lookup_named id env in 
diff --git a/parsing/search.ml b/parsing/search.ml
index de7e497b18..8435f4b4bb 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -34,7 +34,7 @@ open Nametab
 
 let print_constructors indsp fn env nconstr =
   for i = 1 to nconstr do
-    fn (ConstructRef (indsp,i)) env (Inductive.type_of_constructor env (indsp,i))
+    fn (ConstructRef (indsp,i)) env (Inductiveops.type_of_constructor env (indsp,i))
   done
 
 let rec head_const c = match kind_of_term c with
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index cda1169dd7..74795f572c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -18,6 +18,24 @@ open Declarations
 open Environ
 open Reductionops
 
+(* The following three functions are similar to the ones defined in
+   Inductive, but they expect an env *)
+
+let type_of_inductive env ind =
+ let specif = Inductive.lookup_mind_specif env ind in
+  Inductive.type_of_inductive specif
+
+(* Return type as quoted by the user *)
+let type_of_constructor env cstr =
+ let specif =
+  Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+ Inductive.type_of_constructor cstr specif
+
+(* Return constructor types in normal form *)
+let arities_of_constructors env ind =
+ let specif = Inductive.lookup_mind_specif env ind in
+  Inductive.arities_of_constructors ind specif
+
 (* [inductive_family] = [inductive_instance] applied to global parameters *)
 type inductive_family = inductive * constr list
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 9d67089f78..2bc8136787 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -14,6 +14,17 @@ open Declarations
 open Environ
 open Evd
 
+(* The following three functions are similar to the ones defined in
+   Inductive, but they expect an env *)
+
+val type_of_inductive    : env -> inductive -> types
+
+(* Return type as quoted by the user *)
+val type_of_constructor  : env -> constructor -> types
+
+(* Return constructor types in normal form *)
+val arities_of_constructors : env -> inductive -> types array
+
 (* An inductive type with its parameters *)
 type inductive_family
 val make_ind_family : inductive * constr list -> inductive_family
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 5a71b28d8d..a75e48a8e9 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -11,6 +11,7 @@
 open Util
 open Term
 open Inductive
+open Inductiveops
 open Names
 open Reductionops
 open Environ
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 759a0c1a15..2f34957022 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -16,6 +16,7 @@ open Reductionops
 open Type_errors
 open Pretype_errors
 open Inductive
+open Inductiveops
 open Typeops
 
 let meta_type env mv =