From 12667b1bb33e05ab473b8ee8c4ef9aede5fa2600 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 2 Aug 2015 18:41:08 +0200
Subject: Fixing pop_rel_context.

This is necessary for the patch for #4221 (817308ab5) to work.
---
 kernel/environ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 30b28177c..109e3830c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -162,7 +162,7 @@ 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_rel_context = List.skipn n ctxt;
     env_nb_rel = env.env_nb_rel - n }
 
 let fold_named_context f env ~init =
-- 
cgit v1.2.3