Ajout du traducteur

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

4 files changed, 21 insertions, 3 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c136507fb1..267174ad29 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -164,6 +164,9 @@ let parse_args () =
     | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem
     | "-compile-verbose" :: []       -> usage ()
 
+    | "-translate" :: rem -> make_translate true; parse rem
+    | "-ftranslate" :: rem -> make_translate true; translate_file := true; parse rem
+
     | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
     | "-unsafe" :: []       -> usage ()
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 2f6d5c934e..a0b4271f6c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -11,12 +11,14 @@
 (* Parsing of vernacular. *)
 
 open Pp
+open Lexer
 open Util
 open Options
 open System
 open Coqast
 open Vernacexpr
 open Vernacinterp
+open Ppvernacnew
 
 (* The functions in this module may raise (unexplainable!) exceptions.
    Use the module Coqtoplevel, which catches these exceptions
@@ -97,6 +99,10 @@ let parse_phrase (po, verbch) =
 
 let just_parsing = ref false
 
+let pr_comments = function
+  | None -> mt()
+  | Some l -> h 0 (List.fold_left (++) (mt ()) (List.rev l))
+
 let rec vernac interpfun input =
   let (loc,com) = parse_phrase input in
   let rec interp = function
@@ -122,7 +128,13 @@ let rec vernac interpfun input =
 
   in 
   try
-    interp com
+    if do_translate () then
+      let _ = interp com in
+      if !translate_file then
+	msgnl (pr_comments !comments ++ pr_vernac com ++ sep_end) 
+      else
+	msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++ pr_vernac com ++ sep_end)); comments := None
+    else interp com
   with e -> 
     raise (DuringCommandInterp (loc, e))
 
@@ -178,7 +190,10 @@ let compile verbosely f =
 *)
   let ldir,long_f_dot_v = Library.start_library f in
   if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
+  let chano = if Options.do_translate () then open_out (f^".v8") else stdout in
+  let _ = Format.set_formatter_out_channel chano in
   let _ = load_vernac verbosely long_f_dot_v in
+  let _ = close_out chano in
   if Pfedit.get_all_proof_names () <> [] then
     (message "Error: There are pending proofs"; exit 1);
   Library.save_library_to ldir (long_f_dot_v ^ "o")
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0645a87f0b..6a282d5477 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1131,7 +1131,7 @@ let interp c = match c with
   | VernacNotation (inf,c,pl,sc) -> vernac_notation inf c pl sc
 
   (* Gallina *)
-  | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
+  | VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f
   | VernacStartTheoremProof (k,id,t,top,f) ->
       vernac_start_proof k (Some id) t top f
   | VernacEndProof (opaq,idopt) -> vernac_end_proof opaq idopt
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 59e0892511..53434bb8ed 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -170,7 +170,7 @@ type vernac_expr =
 
   (* Gallina *)
   | VernacDefinition of definition_kind * identifier * definition_expr *
-      declaration_hook
+      declaration_hook * definitionkind
   | VernacStartTheoremProof of theorem_kind * identifier *
       (local_binder list * constr_expr) * bool * declaration_hook
   | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option