diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-13 09:38:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-13 12:08:33 +0200 |
| commit | c272523bb9d89fe55d1636b48728e7938a8230dd (patch) | |
| tree | 6a9b4eee3169298d9371c76558189c1d0b27a2d4 /kernel/environ.ml | |
| parent | 54b1d23e062940263b6868945db808d49d011306 (diff) | |
Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index f4420c489..5bd0edf69 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 |