aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/ocamldebug-coq.template (renamed from dev/ocamldebug-v7.template)0
-rwxr-xr-xdev/ocamldebug-v741
2 files changed, 41 insertions, 0 deletions
diff --git a/dev/ocamldebug-v7.template b/dev/ocamldebug-coq.template
index 96c53192d..96c53192d 100644
--- a/dev/ocamldebug-v7.template
+++ b/dev/ocamldebug-coq.template
diff --git a/dev/ocamldebug-v7 b/dev/ocamldebug-v7
new file mode 100755
index 000000000..b3bc324f8
--- /dev/null
+++ b/dev/ocamldebug-v7
@@ -0,0 +1,41 @@
+#!/bin/sh
+
+# wrap around ocamldebug for Coq
+
+export COQTOP=/home/herbelin/coq/V7trad
+export COQLIB=/home/herbelin/coq/V7trad
+export COQTH=$COQLIB/theories
+CAMLBIN=/usr/local/bin
+OCAMLDEBUG=$CAMLBIN/ocamldebug
+export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
+
+args=""
+coqdebug="no"
+for op in $*
+ do case `basename $op` in
+ coq-debug-programs.out)
+ coqdebug="yes"
+ args="-is programs.coq";;
+ *coq*) coqdebug="yes";;
+ esac
+done
+
+case $coqdebug in
+ yes)
+ exec $OCAMLDEBUG \
+ -I $CAMLP4LIB \
+ -I $COQTOP/config \
+ -I $COQTOP/lib -I $COQTOP/kernel \
+ -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
+ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
+ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
+ -I $COQTOP/translate \
+ -I $COQTOP/contrib/correctness \
+ -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
+ -I $COQTOP/contrib/fourier -I $COQTOP/contrib/graphs \
+ -I $COQTOP/contrib/interface -I $COQTOP/contrib/jprover \
+ -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \
+ -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \
+ $* $args;;
+ *) exec $OCAMLDEBUG $*;;
+esac