1 files changed, 0 insertions, 49 deletions
diff --git a/dev/tools/univdot b/dev/tools/univdot
deleted file mode 100755
index bb0dd2c8..00000000
--- 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