diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /kernel/pre_env.mli | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 25 |
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 |