aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
diff options
context:
space:
mode:
Diffstat (limited to 'grammar')
-rw-r--r--grammar/grammar.mllib5
1 files changed, 3 insertions, 2 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index e16f181e6..bdfbbf515 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,8 +1,10 @@
Coq_config
+Int
+Option
+Store
Exninfo
Backtrace
-Int
Pp_control
Flags
Pp
@@ -17,7 +19,6 @@ CArray
Util
Bigint
Predicate
-Option
Segmenttree
Unicodetable
Unicode