Suite restructuration inductifs; changement nom module Constant en Declarations

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

12 files changed, 176 insertions, 188 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index e7b1a634fa..f452a6dfc2 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -309,7 +309,7 @@ let fixp_reducible redfun flgs op stk =
     false
 
 let mindsp_nparams env sp =
-  let mib = lookup_mind sp env in mib.Constant.mind_nparams
+  let mib = lookup_mind sp env in mib.Declarations.mind_nparams
 
 (* The main recursive functions
  *
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 16284de7b2..4f9d4e957e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -8,7 +8,7 @@ open Sign
 open Univ
 open Generic
 open Term
-open Constant
+open Declarations
 open Abstraction
 
 (* The type of environments. *)
@@ -212,13 +212,11 @@ let abst_value env = function
   | _ -> invalid_arg "abst_value"
 
 let defined_constant env = function
-  | DOPN (Const sp, _) ->
-      Constant.is_defined (lookup_constant sp env)
+  | DOPN (Const sp, _) -> is_defined (lookup_constant sp env)
   | _ -> invalid_arg "defined_constant"
 
 let opaque_constant env = function
-  | DOPN (Const sp, _) -> 
-      Constant.is_opaque (lookup_constant sp env)
+  | DOPN (Const sp, _) -> is_opaque (lookup_constant sp env)
   | _ -> invalid_arg "opaque_constant"
 
 (* A const is evaluable if it is defined and not opaque *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 720ff16dc5..8f73b9779b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Names
 open Term
-open Constant
+open Declarations
 open Abstraction
 open Univ
 open Sign
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 9335a63b74..ea8b775703 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -5,7 +5,7 @@ open Util
 open Names
 open Generic
 open Term
-open Constant
+open Declarations
 open Inductive
 open Sign
 open Environ
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 505ea1d955..e73d5779ad 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -5,7 +5,7 @@
 open Names
 open Univ
 open Term
-open Constant
+open Declarations
 open Environ
 (*i*)
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 823e4e612b..4a7649a79c 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -7,11 +7,11 @@ open Univ
 open Generic
 open Term
 open Sign
-open Constant
+open Declarations
 open Environ
 open Reduction
 
-type mind_specif = {
+type inductive_instance = {
   mis_sp : section_path;
   mis_mib : mutual_inductive_body;
   mis_tyi : int;
@@ -19,9 +19,11 @@ type mind_specif = {
   mis_mip : mutual_inductive_packet }
 
 let mis_ntypes mis = mis.mis_mib.mind_ntypes
+let mis_nparams mis = mis.mis_mib.mind_nparams
+
 let mis_index mis = mis.mis_tyi
+
 let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
-let mis_nparams mis = mis.mis_mib.mind_nparams
 let mis_nrealargs mis = mis.mis_mip.mind_nrealargs
 let mis_kelim mis = mis.mis_mip.mind_kelim
 let mis_recargs mis =
@@ -46,16 +48,29 @@ let mis_lc_without_abstractions mis =
   in 
   strip_DLAM (mis_lc mis)
 
+(* gives the vector of constructors and of 
+   types of constructors of an inductive definition 
+   correctly instanciated *)
+
 let mis_type_mconstructs mispec =
   let specif = mis_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
   let make_Ik k = mkMutInd ((mispec.mis_sp,k),mispec.mis_args) 
-  and make_Ck k = mkMutConstruct (((mispec.mis_sp,mispec.mis_tyi),k+1),
+  and make_Ck k = mkMutConstruct
+		    (((mispec.mis_sp,mispec.mis_tyi),k+1),
 		       mispec.mis_args) in
   (Array.init nconstr make_Ck, 
    sAPPVList specif (list_tabulate make_Ik ntypes))
 
+let mis_type_mconstruct i mispec =
+  let specif = mis_lc mispec
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) in 
+  if i > nconstr then error "Not enough constructors in the type";
+  sAPPViList (i-1) specif (list_tabulate make_Ik ntypes)
+
 let mis_typed_arity mis =
   let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
   and largs = Array.to_list mis.mis_args in
@@ -81,33 +96,16 @@ let liftn_inductive_instance n depth mis = {
 
 let lift_inductive_instance n = liftn_inductive_instance n 1
 
-
-type constructor_summary = {
-  cs_cstr : constructor;
-  cs_params : constr list;
-  cs_nargs : int;
-  cs_args : (name * constr) list;
-  cs_concl_realargs : constr array
-}
-
-let lift_constructor n cs = {
-  cs_cstr = (let (csp,ctxt) = cs.cs_cstr in (csp,Array.map (lift n) ctxt));
-  cs_params = List.map (lift n) cs.cs_params;
-  cs_nargs = cs.cs_nargs;
-  cs_args = lift_context n cs.cs_args;
-  cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
+let substn_many_ind_instance cv depth mis = {
+  mis_sp = mis.mis_sp;
+  mis_mib = mis.mis_mib;
+  mis_tyi = mis.mis_tyi;
+  mis_args = Array.map (substn_many cv depth) mis.mis_args;
+  mis_mip = mis.mis_mip
 }
 
 (* [inductive_family] = [inductive_instance] applied to global parameters *)
-type inductive_family = IndFamily of mind_specif * constr list
-(* = {
-  mind : inductive;
-  params : constr list;
-  nparams : int;
-  nrealargs : int;
-  nconstr : int;
-  ind_kelim : sorts list;
-} *)
+type inductive_family = IndFamily of inductive_instance * constr list
 
 type inductive_type = IndType of inductive_family * constr list
 
@@ -119,6 +117,14 @@ let liftn_inductive_type n d (IndType (indf, realargs)) =
   IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs)
 let lift_inductive_type n = liftn_inductive_type n 1
 
+let substn_many_ind_family cv depth (IndFamily (mis,params)) =
+  IndFamily (substn_many_ind_instance cv depth mis,
+	     List.map (substn_many cv depth) params)
+
+let substn_many_ind_type cv depth (IndType (indf,realargs)) =
+  IndType (substn_many_ind_family cv depth indf,
+	   List.map (substn_many cv depth) realargs)
+
 let make_ind_family (mis, params) = IndFamily (mis,params)
 let dest_ind_family (IndFamily (mis,params)) = (mis,params)
 
@@ -160,25 +166,21 @@ let inductive_path_of_constructor_path (ind_sp,i) = ind_sp
 let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)
 
 let inductive_of_constructor ((ind_sp,i),args) = (ind_sp,args)
+let index_of_constructor ((ind_sp,i),args) = i
 let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args)
 
-let build_dependent_constructor cs =
-  applist
-    (mkMutConstruct cs.cs_cstr,
-     (List.map (lift cs.cs_nargs) cs.cs_params)@(rel_list 0 cs.cs_nargs))
-
-let build_dependent_inductive (IndFamily (mis, params)) =
-  let nrealargs = mis_nrealargs mis in
-  applist 
-    (mkMutInd (mis_inductive mis),
-     (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
-
 exception Induc
 
+let extract_mrectype env sigma t =
+  let (t,l) = whd_stack env sigma t [] in
+  match t with
+    | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l)
+    | _ -> raise Induc
+
 let find_mrectype env sigma c =
   let (t,l) = whd_betadeltaiota_stack env sigma c [] in
   match t with
-    | DOPN(MutInd ind_sp,args) ->  ((ind_sp,args),l)
+    | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l)
     | _ -> raise Induc
 
 let find_minductype env sigma c =
@@ -208,10 +210,24 @@ let find_inductive env sigma ty =
   let (params,realargs) = list_chop nparams largs in
   make_ind_type (make_ind_family (mispec,params),realargs)
 
+type constructor_summary = {
+  cs_cstr : constructor;
+  cs_params : constr list;
+  cs_nargs : int;
+  cs_args : (name * constr) list;
+  cs_concl_realargs : constr array
+}
+
+let lift_constructor n cs = {
+  cs_cstr = (let (csp,ctxt) = cs.cs_cstr in (csp,Array.map (lift n) ctxt));
+  cs_params = List.map (lift n) cs.cs_params;
+  cs_nargs = cs.cs_nargs;
+  cs_args = lift_context n cs.cs_args;
+  cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
+}
+
 let get_constructors (IndFamily (mispec,params)) =
-  let specif = mis_lc mispec in
-  let make_ik i = DOPN (MutInd (mispec.mis_sp,i), mispec.mis_args) in
-  let types = sAPPVList specif (list_tabulate make_ik (mis_ntypes mispec)) in
+  let _,types = mis_type_mconstructs mispec in
   let make_ck j =
     let (args,ccl) = decompose_prod (prod_applist types.(j) params) in
     let (_,vargs) = array_chop (mis_nparams mispec + 1) (destAppL (ensure_appl ccl)) in
@@ -226,6 +242,19 @@ let get_arity env sigma (IndFamily (mispec,params)) =
   let arity = mis_arity mispec in
   splay_arity env sigma (prod_applist arity params)
 
+(* Functions to build standard types related to inductive *)
+
+let build_dependent_constructor cs =
+  applist
+    (mkMutConstruct cs.cs_cstr,
+     (List.map (lift cs.cs_nargs) cs.cs_params)@(rel_list 0 cs.cs_nargs))
+
+let build_dependent_inductive (IndFamily (mis, params)) =
+  let nrealargs = mis_nrealargs mis in
+  applist 
+    (mkMutInd (mis_inductive mis),
+     (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
+
 (* builds the arity of an elimination predicate in sort [s] *)
 let make_arity env sigma dep indf s =
   let (arsign,_) = get_arity env sigma indf in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 51ea86f301..b7501dd642 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -6,44 +6,83 @@ open Names
 open Univ
 open Term
 open Sign
-open Constant
+open Declarations
 open Environ
 open Evd
 (*i*)
 
-(*s To give a more efficient access to the informations related to a given
-  inductive type, we introduce the following type [mind_specif], which
-  contains all the informations about the inductive type, including its
-  instanciation arguments. *)
-
-type mind_specif = {
-  mis_sp : section_path;
-  mis_mib : mutual_inductive_body;
-  mis_tyi : int;
-  mis_args : constr array;
-  mis_mip : mutual_inductive_packet }
-
-val mis_index : mind_specif -> int
-val mis_ntypes : mind_specif -> int
-val mis_nconstr : mind_specif -> int
-val mis_nparams : mind_specif -> int
-val mis_nrealargs : mind_specif -> int
-val mis_kelim : mind_specif -> sorts list
-val mis_recargs : mind_specif -> (recarg list) array array
-val mis_recarg : mind_specif -> (recarg list) array
-val mis_typename : mind_specif -> identifier
-val mis_typepath : mind_specif -> section_path
-val mis_is_recursive_subset : int list -> mind_specif -> bool
-val mis_is_recursive : mind_specif -> bool
-val mis_consnames : mind_specif -> identifier array
-val mis_typed_arity : mind_specif -> typed_type
-val mis_inductive : mind_specif -> inductive
-val mis_arity : mind_specif -> constr
-val mis_lc : mind_specif -> constr
-val mis_lc_without_abstractions : mind_specif -> constr array
-val mis_type_mconstructs : mind_specif -> constr array * constr array
-val mis_params_ctxt : mind_specif -> (name * constr) list
-val mis_sort : mind_specif -> sorts
+(*s Inductives are accessible at several stages:
+
+A [mutual_inductive_body] contains all information about a
+declaration of mutual (co-)inductive types. These informations are
+closed (they depend on no free variables) and an instance of them
+corresponds to a [mutual_inductive_instance =
+mutual_inductive_body * constr list]. One inductive type in an
+instanciated packet corresponds to an [inductive_instance =
+mutual_inductive_instance * int]. Applying global parameters to an
+inductive_instance gives an [inductive_family = inductive_instance *
+constr list]. Finally, applying real parameters gives an
+[inductive_type = inductive_family * constr list]. At each level
+corresponds various appropriated functions *)
+
+type inductive_instance (* ex-mind_specif *)
+
+val mis_index : inductive_instance -> int
+val mis_ntypes : inductive_instance -> int
+val mis_nconstr : inductive_instance -> int
+val mis_nparams : inductive_instance -> int
+val mis_nrealargs : inductive_instance -> int
+val mis_kelim : inductive_instance -> sorts list
+val mis_recargs : inductive_instance -> (recarg list) array array
+val mis_recarg : inductive_instance -> (recarg list) array
+val mis_typename : inductive_instance -> identifier
+val mis_typepath : inductive_instance -> section_path
+val mis_is_recursive_subset : int list -> inductive_instance -> bool
+val mis_is_recursive : inductive_instance -> bool
+val mis_consnames : inductive_instance -> identifier array
+val mis_typed_arity : inductive_instance -> typed_type
+val mis_inductive : inductive_instance -> inductive
+val mis_arity : inductive_instance -> constr
+val mis_lc : inductive_instance -> constr
+val mis_lc_without_abstractions : inductive_instance -> constr array
+val mis_type_mconstructs : inductive_instance -> constr array * constr array
+val mis_type_mconstruct : int -> inductive_instance -> constr
+val mis_params_ctxt : inductive_instance -> (name * constr) list
+val mis_sort : inductive_instance -> sorts
+
+(*s [inductive_family] = [inductive_instance] applied to global parameters *)
+type inductive_family = IndFamily of inductive_instance * constr list
+
+val make_ind_family : inductive_instance * constr list -> inductive_family
+val dest_ind_family : inductive_family -> inductive_instance * constr list
+
+val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
+val lift_inductive_family : int -> inductive_family -> inductive_family
+val substn_many_ind_family : constr Generic.substituend array -> int
+  -> inductive_family -> inductive_family
+
+(*s [inductive_type] = [inductive_family] applied to ``real'' parameters *)
+type inductive_type = IndType of inductive_family * constr list
+
+val make_ind_type : inductive_family * constr list -> inductive_type
+val dest_ind_type : inductive_type -> inductive_family * constr list
+
+val mkAppliedInd : inductive_type -> constr
+
+val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
+val lift_inductive_type : int -> inductive_type -> inductive_type
+val substn_many_ind_type : constr Generic.substituend array -> int
+ -> inductive_type -> inductive_type
+
+(*s A [constructor] is an [inductive] + an index; the following functions
+    destructs and builds [constructor] *)
+val inductive_of_constructor : constructor -> inductive
+val index_of_constructor : constructor -> int
+val ith_constructor_of_inductive : inductive -> int -> constructor
+
+val inductive_path_of_constructor_path : constructor_path -> inductive_path
+val ith_constructor_path_of_inductive_path :
+  inductive_path -> int -> constructor_path
 
 (*s This type gathers useful informations about some instance of a constructor
     relatively to some implicit context (the current one)
@@ -65,42 +104,7 @@ type constructor_summary = {
 
 val lift_constructor : int -> constructor_summary -> constructor_summary
 
-(*s A variant of [mind_specif_of_mind] with pre-splitted args
-
-   We recover the inductive type as \par
-   [DOPN(AppL,[|MutInd mind;..params..;..realargs..|])] \par
-   with [mind]  = [((sp,i),localvars)] for some [sp, i, localvars].
-
- *)
-
-(* [inductive_family] = [inductive_instance] applied to global parameters *)
-type inductive_family = IndFamily of mind_specif * constr list
-
-val make_ind_family : mind_specif * constr list -> inductive_family
-val dest_ind_family : inductive_family -> mind_specif * constr list
-
-(* [inductive_type] = [inductive_family] applied to ``real'' parameters *)
-type inductive_type = IndType of inductive_family * constr list
-
-val make_ind_type : inductive_family * constr list -> inductive_type
-val dest_ind_type : inductive_type -> inductive_family * constr list
-
-val mkAppliedInd : inductive_type -> constr
-
-val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
-val lift_inductive_family : int -> inductive_family -> inductive_family
-
-val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
-val lift_inductive_type : int -> inductive_type -> inductive_type
-
-val inductive_of_constructor : constructor -> inductive
-
-val ith_constructor_of_inductive : inductive -> int -> constructor
-
-val inductive_path_of_constructor_path : constructor_path -> inductive_path
-
-val ith_constructor_path_of_inductive_path :
-  inductive_path -> int -> constructor_path
+(*s Functions to build standard types related to inductive *)
 
 (* This builds [(ci params (Rel 1)...(Rel ci_nargs))] which is the argument
    of a dependent predicate in a Cases branch *)
@@ -123,7 +127,8 @@ val make_arity : env -> 'a evar_map -> bool -> inductive_family ->
    [p]; if [dep=true], the predicate is assumed dependent *)
 val build_branch_type : env -> bool -> constr -> constructor_summary -> constr 
 
-(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
+
+(*s [find_m*type env sigma c] coerce [c] to an recursive type (I args).
    [find_mrectype], [find_minductype] and [find_mcoinductype]
    respectively accepts any recursive type, only an inductive type and
    only a coinductive type.
@@ -133,8 +138,9 @@ exception Induc
 val find_mrectype     : env -> 'a evar_map -> constr -> inductive * constr list
 val find_minductype   : env -> 'a evar_map -> constr -> inductive * constr list
 val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list
+val extract_mrectype  : env -> 'a evar_map -> constr -> inductive * constr list
 
-val lookup_mind_specif : inductive -> env -> mind_specif
+val lookup_mind_specif : inductive -> env -> inductive_instance
 
 (* [find_inductive env sigma t] builds an [inductive_type] or raises
    [Induc] if [t] is not an inductive type; The result is relative to
@@ -189,7 +195,6 @@ and [get_arity env sigma is] returns [[(Anonymous,'nat')],'Set'].
 
 (* Cases info *)
 
-val make_case_info : mind_specif -> case_style option -> pattern_source array 
-      -> case_info
-val make_default_case_info : mind_specif -> case_info
-
+val make_case_info : inductive_instance -> case_style option 
+  -> pattern_source array -> case_info
+val make_default_case_info : inductive_instance -> case_info
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 37e2c310c4..94ab793c6a 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -8,7 +8,7 @@ open Generic
 open Term
 open Sign
 open Evd
-open Constant
+open Declarations
 open Environ
 
 let is_id_inst ids args =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 51ba31504b..de61b72e97 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -8,7 +8,7 @@ open Generic
 open Term
 open Univ
 open Evd
-open Constant
+open Declarations
 open Environ
 open Instantiate
 open Closure
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9fc5265e91..1cf6c6eca0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -9,7 +9,7 @@ open Generic
 open Term
 open Reduction
 open Sign
-open Constant
+open Declarations
 open Inductive
 open Environ
 open Type_errors
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index e95aa23908..07857dea96 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -7,7 +7,7 @@ open Names
 open Term
 open Univ
 open Sign
-open Constant
+open Declarations
 open Inductive
 open Environ
 open Typeops
@@ -46,7 +46,7 @@ val lookup_var : identifier -> safe_environment -> name * typed_type
 val lookup_rel : int -> safe_environment -> name * typed_type
 val lookup_constant : section_path -> safe_environment -> constant_body
 val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
-val lookup_mind_specif : inductive -> safe_environment -> mind_specif
+val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
 
 val export : safe_environment -> string -> compiled_env
 val import : compiled_env -> safe_environment -> safe_environment
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 6e453b60b8..b62e31714f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -7,7 +7,7 @@ open Names
 open Univ
 open Generic
 open Term
-open Constant
+open Declarations
 open Sign
 open Environ
 open Reduction
@@ -94,62 +94,21 @@ let instantiate_arity mis =
 let instantiate_arity = mis_typed_arity
 
 let type_of_inductive env sigma i =
-  let mis = lookup_mind_specif i env in
-  let hyps = mis.mis_mib.mind_hyps in
   (* TODO: check args *)
-  instantiate_arity mis
+  instantiate_arity (lookup_mind_specif i env)
 
 (* Constructors. *)
 
-(*
-let instantiate_lc mis =
-  let hyps = mis.mis_mib.mind_hyps in
-  let lc = mis.mis_mip.mind_lc in
-  instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args)
-*)
-let instantiate_lc = mis_lc
-
-let type_of_constructor env sigma ((ind_sp,j),args as cstr) =
-  let mind = inductive_of_constructor cstr in
-  let mis = lookup_mind_specif mind env in
-  (* TODO: check args *)
-  let specif = instantiate_lc mis in
-  let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in
-  if j > mis_nconstr mis then
-    anomaly "type_of_constructor"
-  else
-    sAPPViList (j-1) specif (list_tabulate make_ik (mis_ntypes mis))
-
-(* gives the vector of constructors and of 
-   types of constructors of an inductive definition 
-   correctly instanciated *)
-
-let mis_type_mconstructs mis =
-  let specif = instantiate_lc mis
-  and ntypes = mis_ntypes mis
-  and nconstr = mis_nconstr mis in
-  let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) 
-  and make_ck k = 
-    DOPN (MutConstruct ((mis.mis_sp,mis.mis_tyi),k+1), mis.mis_args) 
-  in
-  (Array.init nconstr make_ck, 
-   sAPPVList specif (list_tabulate make_ik ntypes))
-
 let type_mconstructs env sigma mind =
-  let mis = lookup_mind_specif mind env in 
-  mis_type_mconstructs mis
-
-let mis_type_mconstruct i mispec =
-  let specif = instantiate_lc mispec
-  and ntypes = mis_ntypes mispec
-  and nconstr = mis_nconstr mispec in
-  let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) in 
-  if i > nconstr then error "Not enough constructors in the type";
-  sAPPViList (i-1) specif (list_tabulate make_Ik ntypes)
+  mis_type_mconstructs (lookup_mind_specif mind env)
 
 let type_mconstruct env sigma i mind =
-  let mis = lookup_mind_specif mind env in
-  mis_type_mconstruct i mis
+  mis_type_mconstruct i (lookup_mind_specif mind env)
+
+let type_of_constructor env sigma cstr =
+  type_mconstruct env sigma
+    (index_of_constructor cstr)
+    (inductive_of_constructor cstr)
 
 let type_inst_construct i (IndFamily (mis,globargs)) =
   let tc = mis_type_mconstruct i mis in
@@ -695,10 +654,6 @@ let check_fix env sigma = function
 
 (* Co-fixpoints. *)
 
-let mind_nparams env i =
-  let mis = lookup_mind_specif i env in
-  mis.mis_mib.mind_nparams
-
 let check_guard_rec_meta env sigma nbfix def deftype = 
   let rec codomain_is_coind c  =
     match whd_betadeltaiota env sigma (strip_outer_cast c) with
@@ -736,7 +691,8 @@ let check_guard_rec_meta env sigma nbfix def deftype =
 	| (DOPN (MutConstruct(_,i as cstr_sp),l), args)  ->
             let lra =vlra.(i-1) in 
             let mI = inductive_of_constructor (cstr_sp,l) in
-            let _,realargs = list_chop (mind_nparams env mI) args in
+	    let mis = lookup_mind_specif mI env in
+            let _,realargs = list_chop (mis_nparams mis) args in
             let rec process_args_of_constr l lra =
               match l with
                 | [] -> true