From 9e2cfa798fc4fb0d50433f14eb714d8f90a82b88 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Oct 2006 18:28:19 +0000
Subject: Documentation de "Set Printing Universes", "Print Universes"
 (anciennement "Dump Universes"), "Universe inconsistency", et description
 brève des univers algébriques.

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

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 81663bb918..3684074fde 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -488,9 +488,8 @@ GEXTEND Gram
       | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
 	  VernacDeclareMLModule l
 
-      (* Dump of the universe graph - to file or to stdout *) 
       | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string ->
-	  VernacPrint (PrintUniverses fopt)
+	  error "This command is deprecated, use Print Universes"
 
       | IDENT "Locate"; l = locatable -> VernacLocate l
 
@@ -626,7 +625,8 @@ GEXTEND Gram
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
-      | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]  
+      | IDENT "Implicit"; qid = global -> PrintImplicit qid
+      | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
-- 
cgit v1.2.3