diff options
Diffstat (limited to 'kernel/pre_env.mli')
-rw-r--r-- | kernel/pre_env.mli | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index f40311661..1e95a3564 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Declarations (** The type of environments. *) @@ -45,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; @@ -56,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 @@ -65,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 |