From e7d592ada2d681876d2bcf0a45d4267b3746064f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 15:41:55 +0000
Subject: Mise en place d'un système optionnel de discharge immédiat; prise en
 compte des défs locales dans les arguments des inductifs; nettoyage divers

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

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index ae1bb46cfa..fa3db0b86e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -78,21 +78,16 @@ let type_of_constant = Instantiate.constant_type
 
 (* Inductive types. *)
 
-let instantiate_arity = mis_user_arity
-
 let type_of_inductive env sigma i =
   (* TODO: check args *)
-  instantiate_arity (lookup_mind_specif i env)
+  mis_arity (lookup_mind_specif i env)
 
 (* Constructors. *)
 
-let type_mconstruct env sigma i mind =
-  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)
+  mis_constructor_type
+    (index_of_constructor cstr) 
+    (lookup_mind_specif (inductive_of_constructor cstr) env)
 
 let type_of_existential env sigma ev =
   Instantiate.existential_type sigma ev
-- 
cgit v1.2.3