aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/grammar.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/grammar.mllib')
-rw-r--r--parsing/grammar.mllib4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index ba393e637..0d7cd3649 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -2,13 +2,13 @@ Coq_config
Profile
Pp_control
-Pp
Compat
Flags
+Pp
Segmenttree
Unicodetable
-Util
Errors
+Util
Bigint
Dyn
Hashcons