diff options
| -rw-r--r-- | dev/README | 1 | ||||
| -rw-r--r-- | dev/doc/universes.txt | 24 | ||||
| -rwxr-xr-x | dev/tools/univdot | 49 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 2 |
6 files changed, 10 insertions, 70 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} diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e42fc7599..5ff8e06a6 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -635,9 +635,6 @@ GEXTEND Gram | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> VernacDeclareMLModule (use_locality (), l) - | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string -> - error "This command is deprecated, use Print Universes" - | IDENT "Locate"; l = locatable -> VernacLocate l (* Managing load paths *) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 3d3e10456..b5367048a 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -878,7 +878,7 @@ let rec pr_vernac = function | PrintHintDb -> str"Print Hint *" | PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s | PrintRewriteHintDbName s -> str"Print Rewrite HintDb" ++ spc() ++ str s - | PrintUniverses fopt -> str"Dump Universes" ++ pr_opt str fopt + | PrintUniverses fopt -> str"Print Universes" ++ pr_opt str fopt | PrintName qid -> str"Print" ++ spc() ++ pr_smart_global qid | PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid |