From 2f69234e4cf2a1484aa43dd4d033957abb9078d5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 22 Nov 2008 14:14:12 +0000
Subject: 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
---
 lib/flags.mli | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'lib/flags.mli')

diff --git a/lib/flags.mli b/lib/flags.mli
index 8c16e5b858..db472cccbc 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
-- 
cgit v1.2.3