diff options
Diffstat (limited to 'kernel/pre_env.mli')
-rw-r--r-- | kernel/pre_env.mli | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 23f9a3f41..f626aa0d3 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -8,9 +8,7 @@ open Names open Term -open Context open Declarations -open Univ (** The type of environments. *) @@ -32,7 +30,7 @@ type globals = { env_modtypes : module_type_body MPmap.t} type stratification = { - env_universes : universes; + env_universes : UGraph.t; env_engagement : engagement } @@ -46,9 +44,9 @@ type named_vals = (Id.t * lazy_val) list type env = { env_globals : globals; - env_named_context : named_context; + env_named_context : Context.Named.t; env_named_vals : named_vals; - env_rel_context : rel_context; + env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; env_stratification : stratification; @@ -57,7 +55,7 @@ type env = { indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = named_context * named_vals +type named_context_val = Context.Named.t * named_vals val empty_named_context_val : named_context_val @@ -66,15 +64,15 @@ val empty_env : env (** Rel context *) val nb_rel : env -> int -val push_rel : rel_declaration -> env -> env +val push_rel : Context.Rel.Declaration.t -> env -> env 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 + Context.Named.Declaration.t -> named_context_val -> named_context_val +val push_named : Context.Named.Declaration.t -> env -> env val lookup_named_val : Id.t -> env -> lazy_val val env_of_named : Id.t -> env -> env |