aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ocamldebug-coq.run
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-02-21 09:30:57 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-02-21 09:30:57 +0100
commite91286465973b6ba40d6646c630df8faa73eb8f1 (patch)
tree58a00bf676dfef64452b5ed25c1587997387e237 /dev/ocamldebug-coq.run
parent2b4f249ed0a28cde876f18aacf19f646d8af8fae (diff)
parentb09751b9a1b48541acc9a2daaff9ebc453fc3bf7 (diff)
Merge PR#309: Ltac as a plugin
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 26cfcc8ae..3850c05fd 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -32,6 +32,6 @@ exec $OCAMLDEBUG \
-I $COQTOP/plugins/ring -I $COQTOP/plugins/romega \
-I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \
-I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \
- -I $COQTOP/plugins/xml \
+ -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \
-I $COQTOP/ide \
"$@"