From e5644fac0cce2040961a451eeeda14a88cf5405b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Nov 2003 21:17:00 +0000
Subject: Ajout Print Implicit

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

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 290a1be0e7..965b11bfd5 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -596,7 +596,8 @@ GEXTEND Gram
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
-      | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s ] ]
+      | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
+      | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
-- 
cgit v1.2.3