From 0c68df5ccdacb5d2ed50b533ad613723914dfee7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 24 Nov 2000 16:13:28 +0000
Subject: certains effets disparaissent a la sortie des sections, d'autres non
 (selon Summary.survive_section)

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

(limited to 'parsing')

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 7c4c40aa1e..1d1deed7d7 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -248,7 +248,7 @@ let rec print_library_entry with_values ent =
   match ent with
     | (sp,Lib.Leaf lobj) -> 
 	[< print_leaf_entry with_values sep (sp,lobj) >]
-    | (_,Lib.OpenedSection str) -> 
+    | (_,Lib.OpenedSection (str,_)) -> 
         [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >]
     | (sp,Lib.ClosedSection _) -> 
         [< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp)));
@@ -286,7 +286,7 @@ let list_filter_vec f vec =
 
 let read_sec_context sec =
   let rec get_cxt in_cxt = function
-    | ((sp,Lib.OpenedSection str) as hd)::rest ->
+    | ((sp,Lib.OpenedSection (str,_)) as hd)::rest ->
         if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | [] -> []
     | hd::rest -> get_cxt (hd::in_cxt) rest 
-- 
cgit v1.2.3