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

1 files changed, 9 insertions, 1 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 33b1952c7..307e1026b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -736,12 +736,20 @@ 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;
       optkey=PrimaryTable("Undo");