Restructuration des outils pour les inductifs.

- Les déclarations (mutual_inductive_packet et mutual_inductive_body),
  utilisisées dans Environ vont dans Constant
- Instantiations du context local (mind_specif), instantiation des
  paramètres globaux (inductive_family) et instantiation complète
  (inductive_type, nouveau nom de inductive_summary) vont dans
  Inductive qui est déplacé après réduction
- Certaines fonctions de Typeops et celle traitant des inductifs dans Reduction
  et Instantiate sont regroupées dans Inductive"


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

1 files changed, 2 insertions, 33 deletions

diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 5e48b8e0c..37e2c310c 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -9,7 +9,6 @@ open Term
 open Sign
 open Evd
 open Constant
-open Inductive
 open Environ
 
 let is_id_inst ids args =
@@ -55,28 +54,6 @@ let constant_value env cst =
 	anomalylabstrm "termenv__constant_value"
 	  [< 'sTR "a defined constant with no body." >]
 
-let mis_lc mis =
-  instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
-    (Array.to_list mis.mis_args)
-
-let mis_lc_without_abstractions mis = 
-  let rec strip_DLAM = function
-    | (DLAM (n,c1)) -> strip_DLAM c1 
-    | (DLAMV (n,v)) -> v
-    | _ -> assert false
-  in 
-  strip_DLAM (mis_lc mis)
-
-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 = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) 
-  and make_Ck k = DOPN(MutConstruct((mispec.mis_sp,mispec.mis_tyi),k+1),
-		       mispec.mis_args) in
-  (Array.init nconstr make_Ck, 
-   sAPPVList specif (list_tabulate make_Ik ntypes))
-
 (* Existentials. *)
 
 let name_of_existential n = id_of_string ("?" ^ string_of_int n)
@@ -85,8 +62,8 @@ let existential_type sigma c =
   let (n,args) = destEvar c in
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
-  instantiate_constr (ids_of_sign hyps) info.evar_concl
-    (Array.to_list args)
+  (* TODO: check args [this comment was in Typeops] *)
+  instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
 
 let existential_value sigma c =
   let (n,args) = destEvar c in
@@ -111,11 +88,3 @@ let const_abst_opt_value env sigma c =
 	if evaluable_abst env c then Some (abst_value env c) else None
     | _ -> invalid_arg "const_abst_opt_value"
 
-let mis_typed_arity mis =
-  let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
-  and largs = Array.to_list mis.mis_args in
-  instantiate_type idhyps mis.mis_mip.mind_arity largs
-
-let mis_arity mispec = incast_type (mis_typed_arity mispec)
-
-