aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-29 11:08:09 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-29 11:08:09 +0000
commit442feb2c07f8f5824e814bba504f02c2742637e2 (patch)
tree25a45991d4c52b9265820cbb52137b1c92ad52cd /dev
parentbf7cfcf92c45af9f559f5bf004e9730d96921850 (diff)
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
-rw-r--r--dev/ocamldebug-coq.template2
-rw-r--r--dev/printers.mllib2
2 files changed, 2 insertions, 2 deletions
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 743205888..5358673ff 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -13,7 +13,7 @@ exec $OCAMLDEBUG \
-I $CAMLP4LIB \
-I $COQTOP \
-I $COQTOP/config \
- -I $COQTOP/lib -I $COQTOP/kernel \
+ -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 \
-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
diff --git a/dev/printers.mllib b/dev/printers.mllib
index f93d01daf..c1a95cdb2 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -137,6 +137,6 @@ Tactic_printer
Egrammar
Himsg
Cerrors
-Vernacexpr
+Locality
Vernacinterp
Top_printers