diff options
| author | herbelin | 2006-10-13 20:29:04 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-13 20:29:04 +0000 |
| commit | 0eaf8212746e473e548c8b28d278d318fdc0d842 (patch) | |
| tree | 5aa056f96fa2fd62880936b1b3f74f7f2e3156c6 /dev | |
| parent | 6140f97b57eb8ffb8ee80ab7bef4240905e5446d (diff) | |
Simplification ocamldebug (coq-debug-programs.out obsolète)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9241 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ocamldebug-coq.template | 24 |
1 files changed, 5 insertions, 19 deletions
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 5c4c4475ef..44680d6d6c 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -9,20 +9,7 @@ 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 \ +exec $OCAMLDEBUG \ -I $CAMLP4LIB \ -I $COQTOP/config \ -I $COQTOP/lib -I $COQTOP/kernel \ @@ -30,13 +17,12 @@ case $coqdebug in -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/fourier -I $COQTOP/contrib/first-order \ -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 -I $COQTOP/contrib/funind \ - $* $args;; - *) exec $OCAMLDEBUG $*;; -esac + -I $COQTOP/contrib/rtauto -I $COQTOP/contrib/setoid_ring \ + -I $COQTOP/contrib/recdef -I $COQTOP/contrib/dp \ + $* |