From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 kernel/pre_env.ml | 75 +++++++++++++++++++++++--------------------------------
 1 file changed, 31 insertions(+), 44 deletions(-)

(limited to 'kernel/pre_env.ml')

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 947e4675..dd4d430a 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 8810 2006-05-12 18:50:21Z barras $ *)
+(* $Id: pre_env.ml 10664 2008-03-14 11:27:37Z soubiran $ *)
 
 open Util
 open Names
@@ -26,34 +26,31 @@ type globals = {
   env_constants : constant_key Cmap.t;
   env_inductives : mutual_inductive_body KNmap.t;
   env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body KNmap.t }
+  env_modtypes : module_type_body MPmap.t;
+  env_alias : module_path MPmap.t }
 
 type stratification = {
   env_universes : universes;
   env_engagement : engagement option
 }
 
-type 'a val_kind =   
-  | VKvalue of values
-  | VKaxiom of 'a
-  | VKdef of constr
+type val_kind = 
+    | VKvalue of values * Idset.t
+    | VKnone
 
-type 'a lazy_val = 'a val_kind ref
+type lazy_val = val_kind ref
 
-type rel_val = inv_rel_key lazy_val
-
-type named_val = identifier lazy_val
-
-type named_vals = (identifier * named_val) list
+type named_vals = (identifier * lazy_val) list
 
 type env = {
   env_globals       : globals;
   env_named_context : named_context;
   env_named_vals    : named_vals;
   env_rel_context   : rel_context;
-  env_rel_val       : rel_val list;
+  env_rel_val       : lazy_val list;
   env_nb_rel        : int;
-  env_stratification : stratification }
+  env_stratification : stratification;
+  retroknowledge : Retroknowledge.retroknowledge }
 
 type named_context_val = named_context * named_vals
 
@@ -64,7 +61,8 @@ let empty_env = {
     env_constants = Cmap.empty;
     env_inductives = KNmap.empty;
     env_modules = MPmap.empty;
-    env_modtypes = KNmap.empty };
+    env_modtypes = MPmap.empty;
+    env_alias = MPmap.empty };
   env_named_context = empty_named_context;
   env_named_vals = [];
   env_rel_context = empty_rel_context;
@@ -72,24 +70,20 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = initial_universes;
-    env_engagement = None } }
+    env_engagement = None };
+  retroknowledge = Retroknowledge.initial_retroknowledge }
 
 
 (* Rel context *)
 
 let nb_rel env = env.env_nb_rel
-
+  
 let push_rel d env =
-  let _,body,_ = d in
-  let rval =
-    match body with
-    | None -> ref (VKaxiom env.env_nb_rel)
-    | Some c -> ref (VKdef c)
-  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 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)
@@ -101,16 +95,13 @@ let env_of_rel n env =
     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) =
-  let id,body,_ = d in
-  let rval =
-    match body with
-    | None -> ref (VKaxiom id)
-    | Some c -> ref (VKdef c)
-  in Sign.add_named_decl d ctxt, (id,rval)::vals
+  let id,_,_ = d in
+  let rval = ref VKnone in
+    Sign.add_named_decl d ctxt, (id,rval)::vals
 
 exception ASSERT of Sign.rel_context
 
@@ -118,18 +109,14 @@ 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 =
-    match body with
-    | None -> ref (VKaxiom id)
-    | Some c -> ref (VKdef c)
-  in
-  { env with  
-    env_named_context = Sign.add_named_decl d env.env_named_context;
-    env_named_vals =  (id,rval):: env.env_named_vals }
+  let rval = ref VKnone in
+    { 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)
-  
+  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
  
-- 
cgit v1.2.3