aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ocamldebug-coq.run
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ocamldebug-coq.run')
-rw-r--r--dev/ocamldebug-coq.run20
1 files changed, 18 insertions, 2 deletions
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index f3e60edea..2bec09de2 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -14,11 +14,19 @@
export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
-exec $OCAMLDEBUG \
+GUESS_CHECKER=
+for arg in "$@"; do
+ if [ "${arg##*/}" = coqchk.byte ]; then
+ GUESS_CHECKER=1
+ fi
+done
+
+if [ -z "$GUESS_CHECKER" ]; then
+ exec $OCAMLDEBUG \
-I $CAMLP5LIB -I +threads \
-I $COQTOP \
-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
- -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
+ -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-I $COQTOP/library -I $COQTOP/engine \
-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
-I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
@@ -35,3 +43,11 @@ exec $OCAMLDEBUG \
-I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \
-I $COQTOP/ide \
"$@"
+else
+ exec $OCAMLDEBUG \
+ -I $CAMLP5LIB -I +threads \
+ -I $COQTOP \
+ -I $COQTOP/config -I $COQTOP/clib \
+ -I $COQTOP/lib -I $COQTOP/checker \
+ "$@"
+fi