diff options
| author | Hugo Herbelin | 2014-06-13 09:38:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-13 12:08:33 +0200 |
| commit | c272523bb9d89fe55d1636b48728e7938a8230dd (patch) | |
| tree | 6a9b4eee3169298d9371c76558189c1d0b27a2d4 /kernel | |
| parent | 54b1d23e062940263b6868945db808d49d011306 (diff) | |
Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).
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 } *) |