aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ocamldebug-coq.run
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-21 00:26:02 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-21 00:36:57 +0100
commita581331f26d96d1a037128ae83bebd5e6c27f665 (patch)
treea45c2df2962dffd9ccdab2806f23c717d87d9fdc /dev/ocamldebug-coq.run
parentdf6132c06f9c8480b01f0a269cd1b95bbaa7f912 (diff)
Creating a dedicated ltac/ folder for Hightactics.
Diffstat (limited to 'dev/ocamldebug-coq.run')
-rw-r--r--dev/ocamldebug-coq.run2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index b00d084ed..f9310e076 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -20,7 +20,7 @@ exec $OCAMLDEBUG \
-I $COQTOP/library -I $COQTOP/engine \
-I $COQTOP/pretyping -I $COQTOP/parsing \
-I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
- -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
+ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
-I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \
-I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
-I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \