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
---
 parsing/prettyp.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'parsing')

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index cbb0ba6640..93751cf5dd 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -375,6 +375,7 @@ let list_filter_vec f vec =
   in 
   frec (Array.length vec -1) []
 
+(* This is designed to print the contents of an opened section *)
 let read_sec_context qid =
   let dir =
     try Nametab.locate_section qid
@@ -383,6 +384,8 @@ let read_sec_context qid =
     | ((sp,Lib.OpenedSection (_,_)) as hd)::rest ->
 	let dir' = make_dirpath (wd_of_sp sp) in
         if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+    | ((sp,Lib.ClosedSection (_,_,ctxt)) as hd)::rest ->
+        error "Cannot print the contents of a closed section"
     | [] -> []
     | hd::rest -> get_cxt (hd::in_cxt) rest 
   in
-- 
cgit v1.2.3