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

3 files changed, 9 insertions, 13 deletions

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