aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include3
-rw-r--r--dev/ocamldebug-coq.template2
2 files changed, 3 insertions, 2 deletions
diff --git a/dev/base_include b/dev/base_include
index 1e692defb9..66d91f92e1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -12,7 +12,8 @@
#directory "lib";;
#directory "proofs";;
#directory "tactics";;
-#directory "translate";;
+#directory "printing";;
+#directory "grammar";;
#directory "intf";;
#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 5358673ffe..1a55b804ea 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -12,7 +12,7 @@ OCAMLDEBUG=$CAMLBIN/ocamldebug
exec $OCAMLDEBUG \
-I $CAMLP4LIB \
-I $COQTOP \
- -I $COQTOP/config \
+ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \
-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \
-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
-I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \