Backporting from v8.2 to trunk:

- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.



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

1 files changed, 6 insertions, 1 deletions

diff --git a/lib/flags.mli b/lib/flags.mli
index f0e4103f68..fe1157d881 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -38,6 +38,7 @@ val make_silent : bool -> unit
 val is_silent : unit -> bool
 val is_verbose : unit -> bool
 val silently : ('a -> 'b) -> 'a -> 'b
+val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
@@ -46,9 +47,13 @@ val if_warn : ('a -> unit) -> 'a -> unit
 
 val hash_cons_proofs : bool ref
 
-(* Temporary activate an option ('c must be an atomic type) *)
+(* Temporary activate an option (to activate option [o] on [f x y z],
+   use [with_option o (f x y) z]) *)
 val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
+(* Temporary deactivate an option *)
+val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
+
 (* If [None], no limit *)
 val set_print_hyps_limit : int option -> unit
 val print_hyps_limit : unit -> int option