diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-10 16:25:42 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-10 16:25:42 +0000 |
commit | 44e644894fef453775bdca2492939f1986e8c5b4 (patch) | |
tree | e4ba364d4fbea8dbe9c14a2ebb76986204e475d4 /dev/ocamldebug-v7 | |
parent | 1f2ec6429da2b09b58480c35e175428e39c1c37b (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-x | dev/ocamldebug-v7 | 35 |
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 |