From 18e28049e62ce80a45c8f7bd6f496b502caa8ad1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Sep 2001 16:26:36 +0000
Subject: Rétablissement de Print Section

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1926 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index 9f3ec4f5d6..5995a9600d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -121,6 +121,8 @@ let open_section id =
   if Nametab.exists_section dir then
     errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
   add_entry sp (OpenedSection (id, freeze_summaries()));
+  (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
+  Nametab.push_section dir;
   path_prefix := dir;
   sp
 
-- 
cgit v1.2.3