diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 6 | ||||
| -rw-r--r-- | kernel/environ.mli | 3 |
2 files changed, 9 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index f4420c489d..5bd0edf696 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -152,6 +152,12 @@ let reset_with_named_context (ctxt,ctxtv) env = let reset_context = reset_with_named_context empty_named_context_val +let pop_rel_context n env = + let ctxt = env.env_rel_context in + { env with + env_rel_context = List.firstn (List.length ctxt - n) ctxt; + env_nb_rel = env.env_nb_rel - n } + let fold_named_context f env ~init = let rec fold_right env = match env.env_named_context with diff --git a/kernel/environ.mli b/kernel/environ.mli index 61a4f7327d..1523f40d1f 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -115,6 +115,9 @@ val reset_context : env -> env (** This forgets rel context and sets a new named context *) val reset_with_named_context : named_context_val -> env -> env +(** This removes the [n] last declarations from the rel context *) +val pop_rel_context : int -> env -> env + (** {5 Global constants } {6 Add entries to global environment } *) |