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

4 files changed, 9 insertions, 66 deletions

diff --git a/dev/README b/dev/README
index 0e40e8200..13a7343b5 100644
--- a/dev/README
+++ b/dev/README
@@ -41,7 +41,6 @@ go in directory and call "make"
 Other development tools (directory tools)
 -----------------------
 
-univdot: produces a graph of CIC universes
 Makefile.dir: makefile dedicated to intensive work in a given directory
 Makefile.subdir: makefile dedicated to intensive work in a given subdirectory
 Makefile.devel: utilities to automatically launch coq in various states
diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt
index 65c1e522a..a40706e99 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.
 
diff --git a/dev/tools/univdot b/dev/tools/univdot
deleted file mode 100755
index bb0dd2c89..000000000
--- a/dev/tools/univdot
+++ /dev/null
@@ -1,49 +0,0 @@
-#!/bin/sh
-
-usage() {
-    echo ""
-    echo "usage: univdot [INPUT] [OUTPUT]"
-    echo ""
-    echo "takes the output of Dump Universes \"file\" command"
-    echo "and transforms it to the dot format"
-    echo ""
-    echo "Coq> Dump Universes \"univ.raw\"."
-    echo ""
-    echo "user@host> univdot univ.raw | dot -Tps > univ.ps" 
-    echo ""
-}
-    
-
-# these are dot edge attributes to draw arrows corresponding 
-# to > >= and = edges of the universe graph
-
-GT="[color=red]"
-GE="[color=blue]"
-EQ="[color=black]"
-
-
-# input/output redirection
-case $# in
-  0) ;;
-  1) case $1 in
-       -h|-help|--help) usage
-               exit 0 ;;
-       *) exec < $1 ;;
-     esac ;;
-  2) exec < $1 > $2 ;;
-  *) usage
-     exit 0;;
-esac
-
-
-# dot header
-echo 'digraph G {\
-  size="7.5,10" ;\
-  rankdir = TB ;'
-
-sed -e "s/^\([^ =>]\+\) > \([^ =>]\+\)/\1 -> \2 $GT/" \
-      -e "s/^\([^ =>]\+\) >= \([^ =>]\+\)/\1 -> \2 $GE/" \
-      -e "s/^\([^ =>]\+\) = \([^ =>]\+\)/\1 -> \2 $EQ/" \
-| sed -e "s/\./_/g" 
-
-echo "}"
\ No newline at end of file
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 4fb47bea7..6630be06a 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -977,7 +977,6 @@ $$
 \nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{ident}
 \nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{string}
 \nlsep \TERM{Declare}~\TERM{ML}~\TERM{Module}~\PLUS{\NT{string}}
-\nlsep \TERM{Dump}~\TERM{Universes}~\OPT{\NT{string}}
 \nlsep \TERM{Locate}~\NT{locatable}
 \nlsep \TERM{Add}~\OPT{\TERM{Rec}}~\TERM{LoadPath}~\NT{string}~\OPT{\NT{as-dirpath}}
 \nlsep \TERM{Remove}~\TERM{LoadPath}~\NT{string}