Ajout option translate_syntax pour caractériser l'interprétation du traducteur à proprement parler

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4139 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 12 insertions, 3 deletions

diff --git a/lib/options.ml b/lib/options.ml
index b67f8359de..5725395724 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -24,6 +24,8 @@ let term_quality = ref false
 
 let xml_export = ref false
 
+let dont_load_proofs = ref false
+
 let v7 = ref true
 let v7_only = ref false
 
@@ -34,6 +36,9 @@ let do_translate () = !translate
 let translate_file = ref false
 let p1 = ref true
 
+(* True only when interning from pp*new.ml *)
+let translate_syntax = ref false
+
 (* Silent / Verbose *)
 let silent = ref false
 let make_silent flag = silent := flag; ()
diff --git a/lib/options.mli b/lib/options.mli
index a65958e4f1..db6ee1d5bd 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -23,6 +23,8 @@ val term_quality : bool ref
 
 val xml_export : bool ref
 
+val dont_load_proofs : bool ref
+
 val v7 : bool ref
 val v7_only : bool ref
 
@@ -31,6 +33,7 @@ val make_translate : bool -> unit
 val do_translate : unit -> bool
 val translate_file : bool ref
 val p1 : bool ref
+val translate_syntax : bool ref
 
 val make_silent : bool -> unit
 val is_silent : unit -> bool
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e74405549c..17b947ebd0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -642,8 +642,9 @@ and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr)
 and intern_tactic_seq ist = function
   (* Traducteur v7->v8 *)
   | TacAtom (_,TacReduce (Unfold [_,Ident (_,id)],_))
-      when string_of_id id = "INZ" -> ist.ltacvars, TacId
-
+      when string_of_id id = "INZ" & !Options.translate_syntax
+        -> ist.ltacvars, TacId
+  (* Fin traducteur v7->v8 *)
 
   | TacAtom (loc,t) ->
       let lf = ref ist.ltacvars in
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 83690598d8..f6577dc143 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -771,7 +771,7 @@ let rec pr_vernac = function
       (if i = 1 then mt() else int i ++ str ": ") ++
       (if !Options.p1 then mt () else str "By ") ++
       (if deftac then mt() else str "!! ") ++
-      pr_raw_tactic_goal i tac
+      Options.with_option Options.translate_syntax (pr_raw_tactic_goal i) tac
   | VernacSolveExistential (i,c) ->
       str"Existential " ++ int i ++ pr_lconstrarg c