From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 kernel/pre_env.ml | 52 +++++++++++++++++++++++-----------------------------
 1 file changed, 23 insertions(+), 29 deletions(-)

(limited to 'kernel/pre_env.ml')

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index dd4d430a..b58951e9 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pre_env.ml 10664 2008-03-14 11:27:37Z soubiran $ *)
+(* $Id$ *)
 
 open Util
 open Names
@@ -18,23 +18,22 @@ open Declarations
 (* The type of environments. *)
 
 
-type key = int option ref 
+type key = int option ref
 
 type constant_key = constant_body * key
- 
+
 type globals = {
-  env_constants : constant_key Cmap.t;
-  env_inductives : mutual_inductive_body KNmap.t;
+  env_constants : constant_key Cmap_env.t;
+  env_inductives : mutual_inductive_body Mindmap_env.t;
   env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body MPmap.t;
-  env_alias : module_path MPmap.t }
+  env_modtypes : module_type_body MPmap.t}
 
 type stratification = {
   env_universes : universes;
   env_engagement : engagement option
 }
 
-type val_kind = 
+type val_kind =
     | VKvalue of values * Idset.t
     | VKnone
 
@@ -56,13 +55,12 @@ type named_context_val = named_context * named_vals
 
 let empty_named_context_val = [],[]
 
-let empty_env = { 
+let empty_env = {
   env_globals = {
-    env_constants = Cmap.empty;
-    env_inductives = KNmap.empty;
+    env_constants = Cmap_env.empty;
+    env_inductives = Mindmap_env.empty;
     env_modules = MPmap.empty;
-    env_modtypes = MPmap.empty;
-    env_alias = MPmap.empty };
+    env_modtypes = MPmap.empty};
   env_named_context = empty_named_context;
   env_named_vals = [];
   env_rel_context = empty_rel_context;
@@ -77,25 +75,25 @@ let empty_env = {
 (* Rel context *)
 
 let nb_rel env = env.env_nb_rel
-  
+
 let push_rel d env =
   let rval = ref VKnone in
     { env with
       env_rel_context = add_rel_decl d env.env_rel_context;
       env_rel_val = rval :: env.env_rel_val;
       env_nb_rel = env.env_nb_rel + 1 }
- 
+
 let lookup_rel_val n env =
   try List.nth env.env_rel_val (n - 1)
   with _ -> raise Not_found
-    
+
 let env_of_rel n env =
   { env with
     env_rel_context = Util.list_skipn n env.env_rel_context;
     env_rel_val = Util.list_skipn n env.env_rel_val;
     env_nb_rel = env.env_nb_rel - n
   }
-    
+
 (* Named context *)
 
 let push_named_context_val d (ctxt,vals) =
@@ -103,36 +101,32 @@ let push_named_context_val d (ctxt,vals) =
   let rval = ref VKnone in
     Sign.add_named_decl d ctxt, (id,rval)::vals
 
-exception ASSERT of Sign.rel_context
+exception ASSERT of rel_context
 
-let push_named d env = 
+let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
   assert (env.env_rel_context = []); *)
   let id,body,_ = d in
   let rval = ref VKnone in
-    { env with  
+    { env with
       env_named_context = Sign.add_named_decl d env.env_named_context;
       env_named_vals =  (id,rval):: env.env_named_vals }
 
 let lookup_named_val id env =
   snd(List.find (fun (id',_) -> id = id') env.env_named_vals)
-    
+
 (* Warning all the names should be different *)
 let env_of_named id env = env
- 
+
 (* Global constants *)
 
 let lookup_constant_key kn env =
-  Cmap.find kn env.env_globals.env_constants
+  Cmap_env.find kn env.env_globals.env_constants
 
 let lookup_constant kn env =
-  fst (Cmap.find kn env.env_globals.env_constants)
+  fst (Cmap_env.find kn env.env_globals.env_constants)
 
 (* Mutual Inductives *)
 let lookup_mind kn env =
-  KNmap.find kn env.env_globals.env_inductives
+  Mindmap_env.find kn env.env_globals.env_inductives
 
-let rec scrape_mind env kn = 
-  match (lookup_mind kn env).mind_equiv with
-    | None -> kn
-    | Some kn' -> scrape_mind env kn'
-- 
cgit v1.2.3