aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/printers.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'dev/printers.mllib')
-rw-r--r--dev/printers.mllib14
1 files changed, 7 insertions, 7 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index f4b3d7f6c..107b2904a 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -6,17 +6,17 @@ Compat
Flags
Util
Bigint
-Hashcons
+Hashcons
Dyn
System
-Envars
-Bstack
+Envars
+Bstack
Edit
-Gset
+Gset
Gmap
-Tlm
+Tlm
Gmapl
-Profile
+Profile
Explore
Predicate
Rtree
@@ -107,7 +107,7 @@ Proof_type
Logic
Refiner
Evar_refiner
-Pfedit
+Pfedit
Tactic_debug
Decl_mode
Ppconstr