Redondances

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

1 files changed, 6 insertions, 0 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1feb20e82..f546c1081 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -86,12 +86,15 @@ let type_of_constant env sigma (sp,args) =
 
 (* Inductive types. *)
 
+(* Q: A faire disparaitre ??
 let instantiate_arity mis =
   let ids = ids_of_sign mis.mis_mib.mind_hyps in
   let args = Array.to_list mis.mis_args in 
   let arity = mis.mis_mip.mind_arity in
   { body = instantiate_constr ids arity.body args;
     typ = arity.typ }
+*)
+let instantiate_arity = Instantiate.mis_typed_arity
 
 let type_of_inductive env sigma i =
   let mis = lookup_mind_specif i env in
@@ -101,10 +104,13 @@ let type_of_inductive env sigma i =
 
 (* 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 = Instantiate.mis_lc
 
 let type_of_constructor env sigma ((ind_sp,j),args as cstr) =
   let mind = inductive_of_constructor cstr in