aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/core.dbg1
-rw-r--r--dev/doc/coq-src-description.txt5
2 files changed, 0 insertions, 6 deletions
diff --git a/dev/core.dbg b/dev/core.dbg
index 71d06cdb0..18e82c352 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -16,7 +16,6 @@ load_printer tactics.cma
load_printer vernac.cma
load_printer stm.cma
load_printer toplevel.cma
-load_printer highparsing.cma
load_printer intf.cma
load_printer API.cma
load_printer ltac_plugin.cmo
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index 00e7f5c53..2dbd132da 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -14,11 +14,6 @@ parsing
tactics
toplevel
-highparsing :
-
- Files in parsing/ that cannot be linked too early.
- Contains the grammar rules g_*.ml4
-
Special components
------------------