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, 10 insertions, 9 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 14a5e43034..933fd33cab 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1156,7 +1156,7 @@ let match_aconstr_cases_pattern c (metas_scl,pat) =
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope scopes vars pat =
   try 
-    if !print_no_symbol then raise No_match;
+    if !Options.raw_print or !print_no_symbol then raise No_match;
     let (sc,n) = Symbols.uninterp_cases_numeral pat in
     match Symbols.availability_of_numeral sc (make_current_scopes scopes) with
     | None -> raise No_match
@@ -1165,7 +1165,7 @@ let rec extern_cases_pattern_in_scope scopes vars pat =
         insert_pat_delimiters (CPatNumeral (loc,n)) key
   with No_match ->
   try 
-    if !print_no_symbol then raise No_match;
+    if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_symbol_pattern scopes vars pat
       (Symbols.uninterp_cases_pattern_notations pat)
   with No_match ->
@@ -1222,7 +1222,7 @@ let occur_name na aty =
     | Anonymous -> false
 
 let is_projection nargs = function
-  | Some r when !print_projections ->
+  | Some r when not !Options.raw_print & !print_projections ->
       (try 
 	let n = Recordops.find_projection_nparams r + 1 in
 	if n <= nargs then Some n else None
@@ -1260,6 +1260,7 @@ let explicitize loc inctx impl (cf,f) args =
     | a::args, imp::impl when is_status_implicit imp ->
         let tail = exprec (q+1) (args,impl) in
         let visible =
+          !Options.raw_print or
           (!print_implicits & !print_implicits_explicit_args) or 
 	  (is_significant_implicit a impl tail &
 	  (not (is_inferable_implicit inctx n imp) or
@@ -1285,7 +1286,7 @@ let explicitize loc inctx impl (cf,f) args =
 	if args = [] then f else CApp (loc, (None, f), args)
 
 let rec skip_coercion dest_ref (f,args as app) =
-  if !print_coercions or Options.do_translate () then app
+  if !Options.raw_print or !print_coercions or Options.do_translate () then app
   else
     try
       match dest_ref f with
@@ -1310,9 +1311,9 @@ let extern_app loc inctx impl (cf,f) args =
   if args = [] (* maybe caused by a hidden coercion *) then
     extern_global loc impl f
   else
-  if !print_implicits &
-    not !print_implicits_explicit_args &
-    List.exists is_status_implicit impl
+  if !Options.raw_print or 
+    (!print_implicits & not !print_implicits_explicit_args &
+     List.exists is_status_implicit impl)
   then 
     CAppExpl (loc, (is_projection (List.length args) cf, f), args)
   else
@@ -1332,13 +1333,13 @@ let rec extern_args extern scopes env args subscopes =
 
 let rec extern inctx scopes vars r =
   try 
-    if !print_no_symbol then raise No_match;
+    if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_numeral (Rawterm.loc_of_rawconstr r)
       scopes (Symbols.uninterp_numeral r)
   with No_match ->
 
   try 
-    if !print_no_symbol then raise No_match;
+    if !Options.raw_print or !print_no_symbol then raise No_match;
     extern_symbol scopes vars r (Symbols.uninterp_notations r)
   with No_match -> match r with
   | RRef (loc,ref) ->