From 7e8613d73c589db97c507a7b2c4554bacc72e161 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 20 Sep 2001 23:37:15 +0000
Subject: Amélioration affichage de print_leaf_entry

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2040 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/prettyp.ml | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 109172af4d..7a8571fdcf 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -315,22 +315,30 @@ let print_leaf_entry with_values sep (sp,lobj) =
     | (_,"INDUCTIVE") ->
 	print_inductive sp
     | (_,"AUTOHINT") -> 
-	[< 'sTR" Hint Marker"; 'fNL >]
+(*	[< 'sTR" Hint Marker"; 'fNL >]*)
+	[< >]
     | (_,"GRAMMAR") -> 
-	[< 'sTR" Grammar Marker"; 'fNL >]
+(*	[< 'sTR" Grammar Marker"; 'fNL >]*)
+	[< >]
     | (_,"SYNTAXCONSTANT") -> 
 	print_syntactic_def sep sp
     | (_,"PPSYNTAX") -> 
-	[< 'sTR" Syntax Marker"; 'fNL >]
+(*	[< 'sTR" Syntax Marker"; 'fNL >]*)
+	[< >]
     | (_,"TOKEN") -> 
-	[< 'sTR" Token Marker"; 'fNL >]
+(*	[< 'sTR" Token Marker"; 'fNL >]*)
+	[< >]
     | (_,"CLASS") -> 
-	[< 'sTR" Class Marker"; 'fNL >]
+(*	[< 'sTR" Class Marker"; 'fNL >]*)
+	[< >]
     | (_,"COERCION") -> 
-	[< 'sTR" Coercion Marker"; 'fNL >]
+(*	[< 'sTR" Coercion Marker"; 'fNL >]*)
+	[< >]
     | (_,"REQUIRE") -> 
-	[< 'sTR" Require Marker"; 'fNL >]
+(*	[< 'sTR" Require Marker"; 'fNL >]*)
+	[< >]
     | (_,"END-SECTION") -> [< >]
+    | (_,"STRUCTURE") -> [< >]
     | (_,s) -> 
 	[< 'sTR(string_of_path sp); 'sTR" : ";
            'sTR"Unrecognized object "; 'sTR s; 'fNL >]
-- 
cgit v1.2.3