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 b499ac0c5..9cd940a88 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Declarations open Univ @@ -46,9 +45,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 +56,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 +65,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 |