option -quality

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

4 files changed, 6 insertions, 0 deletions

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 3d8fb71f3e..e401679181 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -50,6 +50,7 @@ val no_red : reds
 val beta_red : reds
 val betaiota_red : reds
 val betadeltaiota_red : reds
+val betaiotazeta_red : reds
 val unfold_red : evaluable_global_reference -> reds
 
 (* Tests if a reduction kind is set *)
diff --git a/lib/options.ml b/lib/options.ml
index b00d523735..d5efe7feff 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -20,6 +20,8 @@ let print_emacs = ref false
 
 let emacs_str s = if !print_emacs then s else "" 
 
+let term_quality = 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 e70d386694..84c60c9ddf 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -19,6 +19,8 @@ val debug : bool ref
 val print_emacs : bool ref
 val emacs_str : string -> string
 
+val term_quality : bool ref
+
 val make_silent : bool -> unit
 val is_silent : unit -> bool
 val is_verbose : unit -> bool
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index befe4cf43b..a88223925f 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -121,6 +121,7 @@ let parse_args () =
 
     | "-batch" :: rem -> set_batch_mode (); parse rem
     | "-boot" :: rem -> boot := true; no_load_rc (); parse rem	     
+    | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem
     | "-outputstate" :: s :: rem -> set_outputstate s; parse rem
     | "-outputstate" :: []       -> usage ()