From de9c86f0ffaf2a290deddb19143f2a326c6771bf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 7 Mar 2000 17:06:09 +0000
Subject: Redondances

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@297 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1feb20e82c..f546c1081b 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
-- 
cgit v1.2.3