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

2 files changed, 9 insertions, 5 deletions

diff --git a/lib/options.ml b/lib/options.ml
index 80b4631233..afa419d679 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -10,6 +10,11 @@
 
 open Util
 
+let with_option o f x =
+  let old = !o in o:=true;
+  try let r = f x in o := old; r
+  with e -> o := old; raise e
+
 let boot = ref false
 
 let batch_mode = ref false
@@ -26,6 +31,8 @@ let xml_export = ref false
 
 let dont_load_proofs = ref false
 
+let raw_print = ref false
+
 let v7 =
   let transl = array_exists ((=) "-translate") Sys.argv in
   let v7 = array_exists ((=) "-v7") Sys.argv in
@@ -66,11 +73,6 @@ let silently f x =
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
 
-let with_option o f x =
-  let old = !o in o:=true;
-  try let r = f x in o := old; r
-  with e -> o := old; raise e
-
 (* The number of printed hypothesis in a goal *)
 
 let print_hyps_limit = ref (None : int option)
diff --git a/lib/options.mli b/lib/options.mli
index 41e8dea844..395efc649a 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -25,6 +25,8 @@ val xml_export : bool ref
 
 val dont_load_proofs : bool ref
 
+val raw_print : bool ref
+
 val v7 : bool ref
 val v7_only : bool ref