From 902ce91fd6006e6df57a8d5133676981967d49b4 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 28 Jun 2015 15:02:22 +0200
Subject: Reinstall Set Printing Universes option overwritten by Maxime!

---
 toplevel/vernacentries.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 04d572cd33..2af28de982 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1433,6 +1433,15 @@ let _ =
       optread  = Pp_control.get_margin;
       optwrite = Pp_control.set_margin }
 
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "printing of universes";
+      optkey   = ["Printing";"Universes"];
+      optread  = (fun () -> !Constrextern.print_universes);
+      optwrite = (fun b -> Constrextern.print_universes:=b) }
+     
 let _ =
   declare_bool_option
     { optsync  = true;
-- 
cgit v1.2.3