From c09da18298d947335cb572ca5f688298b1b8238e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Oct 2006 09:58:16 +0000
Subject: Ajout option Set Printing Universes et amélioration affichage des
 univers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9304 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c72fb248bd..5ae3998f31 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -800,6 +800,14 @@ let _ =
       optread=Pp_control.get_margin;
       optwrite=Pp_control.set_margin }
 
+let _ =
+  declare_bool_option
+    { optsync=true;
+      optkey=SecondaryTable("Printing","Universes");
+      optname="the printing of universes";
+      optread=(fun () -> !Constrextern.print_universes);
+      optwrite=(fun b -> Constrextern.print_universes:=b) }
+
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
 
-- 
cgit v1.2.3