From e5b94c29ff49f8b880290a72519157d26351bc6c Mon Sep 17 00:00:00 2001
From: glondu
Date: Fri, 24 Dec 2010 23:49:15 +0000
Subject: Remove obsolete script univdot, update dev doc about universes

By the way, definitely remove "Dump Universes", which has been
deprecated since 2006 (r9306).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13754 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/universes.txt | 24 +++++++++---------------
 1 file changed, 9 insertions(+), 15 deletions(-)

(limited to 'dev/doc')

diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt
index 65c1e522af..a40706e996 100644
--- a/dev/doc/universes.txt
+++ b/dev/doc/universes.txt
@@ -1,32 +1,26 @@
 How to debug universes?
 
-1. There is a command Dump Universes in Coq toplevel
+1. There is a command Print Universes in Coq toplevel
 
-   Dump Universes.
+   Print Universes.
      prints the graph of universes in the form of constraints
 
-   Dump Universes "file".
+   Print Universes "file".
      produces the "file" containing universe constraints in the form
        univ1 # univ2 ;
      where # can be either > >= or =
-     
-   The file produced by the latter command can be transformed using
-   the script univdot to dot format.
-   For example
 
-   univdot file | dot -Tps > file.ps
-
-   produces a graph of universes in ps format. 
-   > arrows are red, >= blue, and = black.
+   If "file" ends with .gv or .dot, the resulting file will be in
+   dot format.
 
 
    *) for dot see http://www.research.att.com/sw/tools/graphviz/
 
 
 2. There is a printing option
-  
-   Termast.print_universes : bool ref
 
-   which, when set (in ocaml after Drop), makes all pretty-printed
-   Type's annotated with the name of the universe.
+   {Set,Unset} Printing Universes.
+
+   which, when set, makes all pretty-printed Type's annotated with the
+   name of the universe.
 
-- 
cgit v1.2.3