From 5992b93bb503daab9526905dffe2bca1a472b4fc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 29 Jan 2004 15:25:52 +0000
Subject: Ajout option raw_print (Set Printing All) pour desactiver toute
 fonctionnalite de haut niveau de l'affichage

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

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 33b1952c7d..307e1026b6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -736,11 +736,19 @@ let _ =
 let _ =
   declare_bool_option 
     { optsync  = true;
-      optname  = "symbols printing";
+      optname  = "notations printing";
       optkey   = (SecondaryTable ("Printing",if !Options.v7 then "Symbols" else "Notations"));
       optread  = (fun () -> not !Constrextern.print_no_symbol);
       optwrite = (fun b ->  Constrextern.print_no_symbol := not b) }
 
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "raw printing";
+      optkey   = (SecondaryTable ("Printing","All"));
+      optread  = (fun () -> !Options.raw_print);
+      optwrite = (fun b -> Options.raw_print := b) }
+
 let _ =
   declare_int_option
     { optsync=false;
-- 
cgit v1.2.3