aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ocamldebug-v7
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-12-10 16:25:42 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>1999-12-10 16:25:42 +0000
commit44e644894fef453775bdca2492939f1986e8c5b4 (patch)
treee4ba364d4fbea8dbe9c14a2ebb76986204e475d4 /dev/ocamldebug-v7
parent1f2ec6429da2b09b58480c35e175428e39c1c37b (diff)
indications pour les developpeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@231 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/ocamldebug-v7')
-rwxr-xr-xdev/ocamldebug-v735
1 files changed, 25 insertions, 10 deletions
diff --git a/dev/ocamldebug-v7 b/dev/ocamldebug-v7
index bad484c41..dc6c2279d 100755
--- a/dev/ocamldebug-v7
+++ b/dev/ocamldebug-v7
@@ -2,18 +2,33 @@
# wrap around ocamldebug for Coq
-export COQTOP=$constr/V7
+# export COQTOP=`coqtop -where`
+export COQTOP=/users/homepc89/jcf/coq/V7
+export COQLIB=$COQTOP
+export COQTH=$COQLIB/theories
export CAMLP4LIB=`camlp4 -where`
CAMLBIN=`which ocamlc`
OCAMLDEBUG=`dirname $CAMLBIN`/ocamldebug
-exec $OCAMLDEBUG \
- -I $CAMLP4LIB \
- -I $COQTOP/lib \
- -I $COQTOP/dev \
- -I $COQTOP/kernel \
- -I $COQTOP/parsing \
- -I $COQTOP/toplevel \
- $*
-
+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/lib -I $COQTOP/kernel \
+ -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
+ -I $COQTOP/proofs -I $COQTOP/tactics \
+ -I $COQTOP/toplevel -I $COQTOP/dev \
+ $* $args;;
+ *) exec $OCAMLDEBUG $*;;
+esac