aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/grammar.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/grammar.mllib')
-rw-r--r--grammar/grammar.mllib5
1 files changed, 0 insertions, 5 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 296d32dc0..6a265bf4a 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -2,7 +2,6 @@ Coq_config
Hook
Terminal
-Canary
Hashset
Hashcons
CSet
@@ -29,14 +28,11 @@ CStack
Util
Ppstyle
Errors
-Predicate
Segmenttree
Unicodetable
Unicode
Genarg
-Names
-
Stdarg
Constrarg
@@ -47,7 +43,6 @@ Entry
Pcoq
Q_util
-Egramml
Argextend
Tacextend
Vernacextend