aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/printers.mllib
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 20:59:37 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 20:59:37 +0000
commit091824ae0f9bffcdee757bbd048e8a0f63cc5054 (patch)
treed4370325be1dc2ed76139e987034101681527368 /dev/printers.mllib
parent198586739090e63ad65051449f1a80f751c4c08b (diff)
Updated Exninfo to the new Store type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16268 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/printers.mllib')
-rw-r--r--dev/printers.mllib6
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 7db5b5cb9..73bda713a 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