diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 33 |
1 files changed, 14 insertions, 19 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 6144f20cbd..728f28be08 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -33,27 +33,22 @@ type stratification = { 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 } type named_context_val = named_context * named_vals @@ -65,14 +60,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 *) |