Modules dans COQ\!\!\!\!

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

1 files changed, 5 insertions, 8 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 6da58adbc..29b09dde1 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -15,6 +15,7 @@ open Term
 open Declarations
 open Sign
 open Environ
+open Entries
 open Reduction
 open Inductive
 open Type_errors
@@ -242,8 +243,8 @@ let judge_of_cast env cj tj =
 let judge_of_inductive env i =
   let constr = mkInd i in
   let _ =
-    let (sp,_) = i in
-    let mib = lookup_mind sp env in
+    let (kn,_) = i in
+    let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
   make_judge constr (type_of_inductive env i)
 
@@ -258,8 +259,8 @@ let judge_of_inductive env i
 let judge_of_constructor env c =
   let constr = mkConstruct c in
   let _ =
-    let ((sp,_),_) = c in
-    let mib = lookup_mind sp env in
+    let ((kn,_),_) = c in
+    let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
   make_judge constr (type_of_constructor env c)
 
@@ -457,10 +458,6 @@ let infer_v env cv =
  
 (* Typing of several terms. *)
 
-type local_entry =
-  | LocalDef of constr
-  | LocalAssum of constr
-
 let infer_local_decl env id = function
   | LocalDef c -> 
       let (j,cst) = infer env c in