aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-06-10 13:22:44 +0200
committerMatthieu Sozeau2014-06-10 13:22:44 +0200
commit63a8b180232f82ffc45d5e0e2137e5bd6b365e01 (patch)
tree4321c1829110e99428d63afde8b30ed8edf3e417 /dev
parentf02823d9f6de5a8e5706c8433b6e2445cb50222f (diff)
Fix module order in printers.mllib
Diffstat (limited to 'dev')
-rw-r--r--dev/printers.mllib2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 29eae1620a..81fcc8493f 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -107,9 +107,9 @@ Heads
Assumptions
Locusops
Miscops
+Universes
Termops
Namegen
-Universes
Evd
Glob_ops
Redops