diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 41 |
1 files changed, 18 insertions, 23 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 2642bc92..445f4e5f 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 8810 2006-05-12 18:50:21Z barras $ *) +(* $Id: pre_env.mli 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_nb_rel : int; - env_stratification : stratification } + env_globals : globals; + env_named_context : named_context; + env_named_vals : named_vals; + env_rel_context : rel_context; + env_rel_val : lazy_val list; + env_nb_rel : int; + env_stratification : stratification; + retroknowledge : Retroknowledge.retroknowledge } type named_context_val = named_context * named_vals @@ -65,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 -> rel_val +val lookup_rel_val : int -> env -> lazy_val val env_of_rel : int -> env -> env (* Named context *) 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 -> named_val +val lookup_named_val : identifier -> env -> lazy_val val env_of_named : identifier -> env -> env (* Global constants *) @@ -85,5 +82,3 @@ 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 - - |