summaryrefslogtreecommitdiff
path: root/kernel/pre_env.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /kernel/pre_env.mli
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'kernel/pre_env.mli')
-rw-r--r--kernel/pre_env.mli25
1 files changed, 11 insertions, 14 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 445f4e5f..718132b3 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pre_env.mli 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
@@ -49,7 +48,7 @@ type env = {
env_rel_context : rel_context;
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
@@ -63,14 +62,14 @@ val empty_env : env
val nb_rel : env -> int
val push_rel : rel_declaration -> env -> env
val lookup_rel_val : int -> env -> lazy_val
-val env_of_rel : int -> env -> env
+val env_of_rel : int -> env -> env
(* Named context *)
-val push_named_context_val :
+val push_named_context_val :
named_declaration -> named_context_val -> named_context_val
val push_named : named_declaration -> env -> env
val lookup_named_val : identifier -> env -> lazy_val
-val env_of_named : identifier -> env -> env
+val env_of_named : identifier -> env -> env
(* Global constants *)
@@ -80,5 +79,3 @@ val lookup_constant : constant -> env -> constant_body
(* Mutual Inductives *)
val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
-(* Find the ultimate inductive in the [mind_equiv] chain *)
-val scrape_mind : env -> mutual_inductive -> mutual_inductive