Fixed bug in VernacExtend printing + missing vernacular printing rules +

revival of option -translate as a -beautify option.

PS: compilation checked against 11610.



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

15 files changed, 175 insertions, 79 deletions

diff --git a/CHANGES b/CHANGES
index 64f51f1d7..c346fc8b3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,9 +1,18 @@
 Changes since V8.2
 ==================
 
+Tactics
+
 - "discriminate" now performs intros before trying to discriminate an
   hypothesis of the goal (previously it applied intro only if the goal
   had the form t1<>t2).
+- rewrite now supports rewriting on ad hoc equalities such as eq_true.
+
+Tools
+
+- New coqtop/coqc option -beautify to reformat .v files (usable
+  e.g. to globally update notations).
+- New tool beautify-archive to beautify a full archive of developments.
 
 Changes from V8.1 to V8.2
 =========================
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 193805b98..d89d855b3 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -27,7 +27,13 @@ END
 open Table
 open Extract_env
 
+let pr_language = function
+  | Ocaml -> str "Ocaml" 
+  | Haskell -> str "Haskell"
+  | Scheme -> str "Scheme"
+
 VERNAC ARGUMENT EXTEND language
+PRINTED BY pr_language
 | [ "Ocaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index a8ad2498d..654474b32 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -129,25 +129,52 @@ ARGUMENT EXTEND auto_using'
 | [ ] -> [ [] ]
 END
 
+let pr_rec_annotation2_aux s r id l =
+  str ("{"^s^" ") ++ Ppconstr.pr_constr_expr r ++ 
+    Util.pr_opt Nameops.pr_id id ++ 
+    Pptactic.pr_auto_using Ppconstr.pr_constr_expr l ++ str "}"
+
+let pr_rec_annotation2 = function
+  | Struct id -> str "{struct" ++ Nameops.pr_id id ++ str "}"
+  | Wf(r,id,l) -> pr_rec_annotation2_aux "wf" r id l
+  | Mes(r,id,l) -> pr_rec_annotation2_aux "measure" r id l
+
 VERNAC ARGUMENT EXTEND rec_annotation2
+PRINTED BY pr_rec_annotation2
   [ "{"  "struct" ident(id)  "}"] -> [ Struct id ]
 | [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ]
 | [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] 
 END
 
+let pr_binder2 (idl,c) =
+  str "(" ++ Util.prlist_with_sep spc Nameops.pr_id idl ++ spc () ++ 
+    str ": " ++ Ppconstr.pr_lconstr_expr c ++ str ")"
 
 VERNAC ARGUMENT EXTEND binder2
-    [ "(" ne_ident_list(idl) ":" lconstr(c)  ")"] ->
-     [
-       LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ]
+PRINTED BY pr_binder2
+    [ "(" ne_ident_list(idl) ":" lconstr(c)  ")"] -> [ (idl,c) ]
 END
 
+let make_binder2 (idl,c) =
+  LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c)
+
+let pr_rec_definition2 (id,bl,annot,type_,def) =
+  Nameops.pr_id id ++ spc () ++ Util.prlist_with_sep spc pr_binder2 bl ++ 
+    Util.pr_opt pr_rec_annotation2 annot ++ spc () ++ str ":" ++ spc () ++
+    Ppconstr.pr_lconstr_expr type_ ++ str " :=" ++ spc () ++ 
+    Ppconstr.pr_lconstr_expr def
 
 VERNAC ARGUMENT EXTEND rec_definition2
- [ ident(id)  binder2_list( bl)
-     rec_annotation2_opt(annot) ":" lconstr( type_)
+PRINTED BY pr_rec_definition2
+ [ ident(id)  binder2_list(bl)
+     rec_annotation2_opt(annot) ":" lconstr(type_)
 	":=" lconstr(def)] ->
-    [let names = List.map snd (Topconstr.names_of_local_assums bl) in
+    [ (id,bl,annot,type_,def) ]
+END
+
+let make_rec_definitions2 (id,bl,annot,type_,def) =
+     let bl = List.map make_binder2 bl in
+     let names = List.map snd (Topconstr.names_of_local_assums bl) in
      let check_one_name () =
        if List.length names > 1 then
          Util.user_err_loc
@@ -174,34 +201,27 @@ VERNAC ARGUMENT EXTEND rec_definition2
 	 | Some an ->
 	     check_exists_args an
      in
-     ((Util.dummy_loc,id), ni, bl, type_, def) ]
-      END
-
-
-VERNAC ARGUMENT EXTEND rec_definitions2
-| [ rec_definition2(rd) ] -> [ [rd] ]
-| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ]
-END
+     ((Util.dummy_loc,id), ni, bl, type_, def)
 
 
 VERNAC COMMAND EXTEND Function
-   ["Function" rec_definitions2(recsl)] ->
+   ["Function" ne_rec_definition2_list_sep(recsl,"with")] ->
 	[ 
-	  do_generate_principle false  recsl; 
+	  do_generate_principle false (List.map make_rec_definitions2 recsl); 
 	  
 	]
 END
 
+let pr_fun_scheme_arg (princ_name,fun_name,s) = 
+  Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ 
+  Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ 
+  Ppconstr.pr_rawsort s
 
 VERNAC ARGUMENT EXTEND fun_scheme_arg
+PRINTED BY pr_fun_scheme_arg
 | [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] 
 END 
 
-VERNAC ARGUMENT EXTEND fun_scheme_args
-| [ fun_scheme_arg(fa) ] -> [ [fa] ] 
-| [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas]
-END 
-
 
 let warning_error names e = 
   match e with 
@@ -219,7 +239,7 @@ let warning_error names e =
 
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
-   ["Functional" "Scheme" fun_scheme_args(fas) ] ->
+   ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] ->
     [
       begin
 	try 
diff --git a/lib/flags.ml b/lib/flags.ml
index 76ab9fe64..f4b36c6c3 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -33,13 +33,10 @@ let raw_print = ref false
 let unicode_syntax = ref false
 
 (* Translate *)
-let translate = ref false
-let make_translate f = translate := f
-let do_translate () = !translate
-let translate_file = ref false
-
-(* True only when interning from pp*new.ml *)
-let translate_syntax = ref false
+let beautify = ref false
+let make_beautify f = beautify := f
+let do_beautify () = !beautify
+let beautify_file = ref false
 
 (* Silent / Verbose *)
 let silent = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 8c16e5b85..db472cccb 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -29,11 +29,10 @@ val raw_print : bool ref
 
 val unicode_syntax : bool ref
 
-val translate : bool ref
-val make_translate : bool -> unit
-val do_translate : unit -> bool
-val translate_file : bool ref
-val translate_syntax : bool ref
+val beautify : bool ref
+val make_beautify : bool -> unit
+val do_beautify : unit -> bool
+val beautify_file : bool ref
 
 val make_silent : bool -> unit
 val is_silent : unit -> bool
diff --git a/lib/util.ml b/lib/util.ml
index 46969ec83..639d2bf00 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1321,7 +1321,7 @@ let prvect_with_sep sep elem v =
 let prvect elem v = prvect_with_sep mt elem v
 
 let pr_located pr (loc,x) =
-  if Flags.do_translate() && loc<>dummy_loc then
+  if Flags.do_beautify() && loc<>dummy_loc then
     let (b,e) = unloc loc in
     comment b ++ pr x ++ comment e
   else pr x
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 770a54a78..7f2a6dd48 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -163,16 +163,27 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl =
     end
   >>
 
-let declare_vernac_argument loc s cl =
+let declare_vernac_argument loc s pr cl =
   let se = mlexpr_of_string s in
+  let wit = <:expr< $lid:"wit_"^s$ >> in
   let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
+  let globwit = <:expr< $lid:"globwit_"^s$ >> in
   let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
+  let pr_rules = match pr with
+    | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >>
+    | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in
   <:str_item<
     declare
-      value $lid:"rawwit_"^s$ = let (_,_,x) = Genarg.create_arg $se$ in x;
+      value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel),
+             ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel),
+              $lid:"rawwit_"^s$) = Genarg.create_arg $se$;
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
       Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None 
         [(None, None, $rules$)];
+      Pptactic.declare_extra_genarg_pprule
+        ($rawwit$, $pr_rules$)
+        ($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer")
+        ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer");
     end
   >>
 
@@ -202,11 +213,12 @@ EXTEND
 	    failwith "Argument entry names must be lowercase";
          declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l
       | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
+        pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr];
         OPT "|"; l = LIST1 argrule SEP "|";
         "END" ->
 	  if String.capitalize s = s then
 	    failwith "Argument entry names must be lowercase";
-         declare_vernac_argument loc s l ] ]
+         declare_vernac_argument loc s pr l ] ]
   ;
   argtype:
     [ "2" 
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 26377013f..5984f7415 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -237,7 +237,7 @@ let rec string bp len = parser
 let xml_output_comment = ref (fun _ -> ())
 let set_xml_output_comment f = xml_output_comment := f
 
-(* Utilities for comment translation *)
+(* Utilities for comments in beautify *)
 let comment_begin = ref None
 let comm_loc bp = if !comment_begin=None then comment_begin := Some bp
 
@@ -280,7 +280,7 @@ let comment_stop ep =
   if !Flags.xml_export && Buffer.length current > 0 &&
     (!between_com || not(null_comment current_s)) then
       !xml_output_comment current_s;
-  (if Flags.do_translate() && Buffer.length current > 0 &&
+  (if Flags.do_beautify() && Buffer.length current > 0 &&
     (!between_com || not(null_comment current_s)) then
     let bp = match !comment_begin with
         Some bp -> bp
@@ -315,7 +315,7 @@ let rec comment bp = parser bp2
          | [< '')' >] -> push_string "*)";
          | [< s >] -> real_push_char '*'; comment bp s >] -> ()
   | [< ''"'; s >] ->
-      if Flags.do_translate() then (push_string"\"";comm_string bp2 s)
+      if Flags.do_beautify() then (push_string"\"";comm_string bp2 s)
       else ignore (string bp2 0 s);
       comment bp s
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
@@ -405,7 +405,7 @@ let rec next_token = parser bp
       (("METAIDENT", get_buff len), (bp,ep))
   | [< ''.' as c; t = parse_after_dot bp c >] ep ->
       comment_stop bp;
-      if Flags.do_translate() & t=("",".") then between_com := true;
+      if Flags.do_beautify() & t=("",".") then between_com := true;
       (t, (bp,ep))
   | [< ''?'; s >] ep ->
       let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 19446b7d1..f5fe151ed 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -101,7 +101,7 @@ let pr_generalization bk ak c =
     str "`" ++ str hd ++ c ++ str tl
 
 let pr_com_at n =
-  if Flags.do_translate() && n <> 0 then comment n 
+  if Flags.do_beautify() && n <> 0 then comment n 
   else mt()
 
 let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0fc28d35f..01e44f84c 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -331,7 +331,7 @@ let pr_assumption_token many = function
       str (if many then "Parameters" else "Parameter")
   | (Global,Conjectural) -> str"Conjecture"
   | (Local,Conjectural) -> 
-      anomaly "Don't know how to translate a local conjecture"
+      anomaly "Don't know how to beautify a local conjecture"
 
 let pr_params pr_c (xl,(c,t)) =
   hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
@@ -612,7 +612,7 @@ let rec pr_vernac = function
       let pr_onerec = function
         | ((loc,id),(n,ro),bl,type_,def),ntn ->
             let (bl',def,type_) =
-              if Flags.do_translate() then extract_def_binders def type_
+              if Flags.do_beautify() then extract_def_binders def type_
               else ([],def,type_) in
             let bl = bl @ bl' in
             let ids = List.flatten (List.map name_of_binder bl) in
@@ -644,7 +644,7 @@ let rec pr_vernac = function
   | VernacCoFixpoint (corecs,b) ->
       let pr_onecorec (((loc,id),bl,c,def),ntn) =
         let (bl',def,c) =
-              if Flags.do_translate() then extract_def_binders def c
+              if Flags.do_beautify() then extract_def_binders def c
               else ([],def,c) in
         let bl = bl @ bl' in
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
@@ -942,19 +942,16 @@ and pr_extend s cl =
     let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
     let start,rl,cl =
       match rl with
-	| Egrammar.TacTerm s :: rl -> str s, rl, cl
-	| Egrammar.TacNonTerm _ :: rl ->
-	    (* Will put an unnecessary extra space in front *)
-	    pr_gen (Global.env()) (List.hd cl), rl, List.tl cl 
-	| [] -> anomaly "Empty entry" in
+      | Egrammar.TacTerm s :: rl -> str s, rl, cl
+      | Egrammar.TacNonTerm _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl 
+      | [] -> anomaly "Empty entry" in
     let (pp,_) =
       List.fold_left
         (fun (strm,args) pi ->
-          match pi with
-              Egrammar.TacNonTerm _ -> 
-                (strm ++ pr_gen (Global.env()) (List.hd args),
-                List.tl args)
-            | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args))
+          let pp,args = match pi with
+          | Egrammar.TacNonTerm _ -> (pr_arg (List.hd args), List.tl args)
+          | Egrammar.TacTerm s -> (str s, args) in
+          (strm ++ spc() ++ pp), args)
         (start,cl) rl in
     hov 1 pp
   with Not_found ->
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 29e30bca7..f661800a1 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -118,6 +118,9 @@ EXTEND
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let t, g = Q_util.interp_entry_name loc e "" in
         VernacNonTerm (loc, t, g, Some s)
+      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
+        let t, g = Q_util.interp_entry_name loc e sep in
+        VernacNonTerm (loc, t, g, Some s)
       | s = STRING ->
         VernacTerm s
     ] ]
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index aa09219bf..ca1763ce2 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -153,7 +153,7 @@ let parse_args () =
       | "-debugVM"|"-alltransp"|"-VMno"
       |"-batch"|"-nois" | "-noglob" | "-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
-      |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate" |"-strict-implicit"
+      |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-impredicative-set"|"-vm" 
       | "-unboxed-values" | "-unboxed-definitions" | "-draw-vm-instr" 
 	  as o) :: rem ->
diff --git a/tools/beautify-archive b/tools/beautify-archive
new file mode 100644
index 000000000..aac6f3e0e
--- /dev/null
+++ b/tools/beautify-archive
@@ -0,0 +1,52 @@
+#!/bin/sh
+
+#This script compiles and beautifies an archive, check the correctness
+#of beautified files, then replace the original files by the
+#beautified ones, keeping a copy of original files in $OLDARCHIVE.
+#The script assumes:
+#- that the archive provides a Makefile built by coq_makefile,
+#- that coqc is in the path or that variables COQTOP and COQBIN are set.
+
+OLDARCHIVE=old_files
+NEWARCHIVE=beautify_files
+BEAUTIFYSUFFIX=.beautified
+
+if [ -e $OLDARCHIVE ]; then
+  echo "Warning: $OLDARCHIVE directory found, the files are maybe already beautified";
+  sleep 5;
+fi
+echo ---- Producing beautified files in the beautification directory -------
+if [ -e $NEWARCHIVE ]; then rm -r $NEWARCHIVE; fi
+if [ -e /tmp/$OLDARCHIVE.$$ ]; then rm -r /tmp/$OLDARCHIVE.$$; fi
+cp -pr . /tmp/$OLDARCHIVE.$$
+cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE
+cd $NEWARCHIVE
+rm description || true
+make clean
+make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
+ { echo ---- Failed to beautify; exit 1; }
+echo -------- Upgrading files in the beautification directory --------------
+beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX`
+for i in $beaufiles; do
+  j=`dirname $i`/`basename $i .v$BEAUTIFYSUFFIX`.v
+  echo Upgrading $j in the beautification directory
+  mv -u -f $i $j
+done
+echo ---- Recompiling beautified files in the beautification directory -----
+make clean
+make || { echo ---- Failed to recompile; exit 1; }
+echo ----- Saving old files in directory $OLDARCHIVE -------------------------
+/bin/rm -r ../$OLDARCHIVE
+mv /tmp/$OLDARCHIVE.$$ ../$OLDARCHIVE
+echo Saving $OLDARCHIVE files done
+echo --------- Upgrading files in current directory ------------------------
+vfiles=`find . -name \*.v`
+cd ..
+for i in $vfiles; do
+  echo Upgrading $i in current directory
+  mv -u -f $NEWARCHIVE/$i $i
+done
+echo -------- Beautification completed -------------------------------------
+echo Old files are in directory '"$OLDARCHIVE"'
+echo New files are in current directory
+echo You can now remove the beautification directory '"$NEWARCHIVE"'
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 2ad5117b9..b2589d42f 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -85,8 +85,8 @@ let add_load_vernacular verb s =
 let load_vernacular () =
   List.iter
     (fun (s,b) -> 
-      if Flags.do_translate () then
-	with_option translate_file (Vernac.load_vernac b) s
+      if Flags.do_beautify () then
+	with_option beautify_file (Vernac.load_vernac b) s
       else
 	Vernac.load_vernac b s)
     (List.rev !load_vernacular_list)
@@ -115,8 +115,8 @@ let compile_files () =
       (fun (v,f) ->
 	 States.unfreeze init_state;
 	 Dumpglob.coqdoc_unfreeze coqdoc_init_state;
-	 if Flags.do_translate () then
-	   with_option translate_file (Vernac.compile v) f
+	 if Flags.do_beautify () then
+	   with_option beautify_file (Vernac.compile v) f
 	 else
 	   Vernac.compile v f)
       (List.rev !compile_list)
@@ -260,7 +260,7 @@ let parse_args is_ide =
 
     | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem
 
-    | "-translate" :: rem -> make_translate true; parse rem
+    | "-beautify" :: rem -> make_beautify true; parse rem
 
     | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
     | "-unsafe" :: []       -> usage ()
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 92d2bbf28..cdfa85328 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -93,23 +93,24 @@ let parse_phrase (po, verbch) =
  * parses, and is verbose on "primitives" commands if verbosely is true *)
 
 let just_parsing = ref false
-let chan_translate = ref stdout
+let chan_beautify = ref stdout
+let beautify_suffix = ".beautified"
 
 let set_formatter_translator() =
-  let ch = !chan_translate in
+  let ch = !chan_beautify in
   let out s b e = output ch s b e in
   Format.set_formatter_output_functions out (fun () -> flush ch);
   Format.set_max_boxes max_int
 
 let pr_new_syntax loc ocom =
   let loc = unloc loc in
-  if !translate_file then set_formatter_translator();
+  if !beautify_file then set_formatter_translator();
   let fs = States.freeze () in
   let com = match ocom with
     | Some VernacNop -> mt()
     | Some com -> pr_vernac com
     | None -> mt() in
-  if !translate_file then
+  if !beautify_file then
     msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
     msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
@@ -121,30 +122,30 @@ let rec vernac_com interpfun (loc,com) =
     | VernacLoad (verbosely, fname) ->
 	let fname = expand_path_macros fname in
         (* translator state *)
-        let ch = !chan_translate in
+        let ch = !chan_beautify in
         let cs = Lexer.com_state() in
         let cl = !Pp.comments in
         (* end translator state *)
         (* coqdoc state *)
         let cds = Dumpglob.coqdoc_freeze() in
-          if !Flags.translate_file then 
+          if !Flags.beautify_file then 
 	    begin
               let _,f = find_file_in_path (Library.get_load_paths ())
 		(make_suffix fname ".v") in
-		chan_translate := open_out (f^"8");
+		chan_beautify := open_out (f^beautify_suffix);
 		Pp.comments := []
             end;
           begin 
 	    try
 	      read_vernac_file verbosely (make_suffix fname ".v");
-              if !Flags.translate_file then close_out !chan_translate;
-              chan_translate := ch;
+              if !Flags.beautify_file then close_out !chan_beautify;
+              chan_beautify := ch;
               Lexer.restore_com_state cs;
               Pp.comments := cl;
               Dumpglob.coqdoc_unfreeze cds
 	    with e -> 
-	      if !Flags.translate_file then close_out !chan_translate;
-              chan_translate := ch;
+	      if !Flags.beautify_file then close_out !chan_beautify;
+              chan_beautify := ch;
               Lexer.restore_com_state cs;
               Pp.comments := cl;
               Dumpglob.coqdoc_unfreeze cds;
@@ -164,7 +165,7 @@ let rec vernac_com interpfun (loc,com) =
 
   in 
     try
-      if do_translate () then pr_new_syntax loc (Some com);
+      if do_beautify () then pr_new_syntax loc (Some com);
       interp com
     with e -> 
       Format.set_formatter_out_channel stdout;
@@ -191,7 +192,7 @@ and read_vernac_file verbosely s =
     close_input in_chan input;    (* we must close the file first *)
     match real_error e with
       | End_of_input ->
-          if do_translate () then pr_new_syntax (make_loc (max_int,max_int)) None
+          if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname e
 
 (* raw_do_vernac : char Stream.t -> unit
@@ -214,13 +215,13 @@ let set_xml_end_library f = xml_end_library := f
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
-  chan_translate :=
-    if !Flags.translate_file then open_out (file^"8") else stdout;
+  chan_beautify :=
+    if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
   try 
     read_vernac_file verb file;
-    if !Flags.translate_file then close_out !chan_translate;
+    if !Flags.beautify_file then close_out !chan_beautify;
   with e -> 
-    if !Flags.translate_file then close_out !chan_translate;
+    if !Flags.beautify_file then close_out !chan_beautify;
     raise_with_file file e
 
 (* Compile a vernac file (f is assumed without .v suffix) *)