aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/printers.mllib6
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 7db5b5cb99..73bda713a6 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -1,8 +1,10 @@
Coq_config
+Int
+Option
+Store
Exninfo
Backtrace
-Int
Pp_control
Loc
Compat
@@ -24,7 +26,6 @@ Dyn
CUnix
System
Envars
-Store
Gmap
Fset
Fmap
@@ -34,7 +35,6 @@ Explore
Predicate
Rtree
Heap
-Option
Dnet
Names