summaryrefslogtreecommitdiff
path: root/dev/ocamldebug-coq.template
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ocamldebug-coq.template')
-rw-r--r--dev/ocamldebug-coq.template42
1 files changed, 42 insertions, 0 deletions
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
new file mode 100644
index 00000000..30224216
--- /dev/null
+++ b/dev/ocamldebug-coq.template
@@ -0,0 +1,42 @@
+#!/bin/sh
+
+# wrap around ocamldebug for Coq
+
+export COQTOP=COQTOPDIRECTORY
+export COQLIB=COQLIBDIRECTORY
+export COQTH=$COQLIB/theories
+CAMLBIN=CAMLBINDIRECTORY
+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 \
+ -I $COQTOP/contrib/subtac \
+ $* $args;;
+ *) exec $OCAMLDEBUG $*;;
+esac