aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/grammar.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/grammar.mllib')
-rw-r--r--parsing/grammar.mllib5
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 226ef4b36..27ca281c8 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -14,15 +14,10 @@ Dyn
Hashcons
Predicate
Option
-Hashtbl_alt
Names
Univ
-Esubst
-Term
-Mod_subst
-Nameops
Libnames
Summary
Genarg