From 4c18a78b54ff33361990a6f19bcad69bb7a4417c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 13 Nov 2003 17:16:30 +0000
Subject: Traduction Print Grammar

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

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 42c518e5a9..9162049688 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -994,7 +994,8 @@ let rec pr_vernac = function
 	| PrintSectionContext s ->
             str"Print Section" ++ spc() ++ Libnames.pr_reference s
 	| PrintGrammar (uni,ent) ->
-            str"Print Grammar" ++ spc() ++ str uni ++ spc() ++ str ent
+            msgerrnl (str "warning: no direct translation of Print Grammar entry"); 
+            str"Print Grammar" ++ spc() ++ str ent
 	| PrintLoadPath -> str"Print LoadPath"
 	| PrintModules -> str"Print Modules"
 	| PrintMLLoadPath -> str"Print ML Path"
-- 
cgit v1.2.3