From f0f5d9983a055e4c0f5215ad7172023b37e946c8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 20 Nov 2004 20:07:38 +0000
Subject: 'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marche

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6333 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernacnew.ml4 | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 2346ae0849..1ce6f16ba7 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -594,7 +594,7 @@ GEXTEND Gram
       | IDENT "Hint"; qid = global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
-      | IDENT "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
+      | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
       | IDENT "Setoids" -> PrintSetoids
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
@@ -723,7 +723,10 @@ GEXTEND Gram
       | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
       | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
-      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
+      | IDENT "only"; x = [ 
+          IDENT "parsing" -> SetOnlyParsing
+        | IDENT "printing" -> SetOnlyPrinting
+        ] -> x
       | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s ] ]
   ;
   syntax_extension_type:
-- 
cgit v1.2.3