aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/parsing.mllib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-09 16:08:50 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-10 19:28:24 +0200
commit6150d15647afc739329019f7e9de595187ecc282 (patch)
tree9dd5b05f3063e9ae0a0660089e6edb8c17e727b2 /parsing/parsing.mllib
parent9891f2321f13861e3f48ddb28abcd5a77be30791 (diff)
Removing the Entry module now that rules need not be marshalled.
Diffstat (limited to 'parsing/parsing.mllib')
-rw-r--r--parsing/parsing.mllib1
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index b052b6ee6..0e1c79c91 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,7 +1,6 @@
Tok
Compat
CLexer
-Entry
Pcoq
Egramml
Egramcoq