Merge PR #9676: Move test_mode from Flags to Vernacentries (use point)

Reviewed-by: ejgallego

5 files changed, 8 insertions, 8 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 1195b8caf1..6718e7a954 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -43,8 +43,6 @@ let with_options ol f x =
 
 let record_aux_file = ref false
 
-let test_mode = ref false
-
 let async_proofs_worker_id = ref "master"
 let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 2b4446a1db..bf8846417b 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -35,10 +35,6 @@
     be eventually removed by cleanups such as PR#1103 *)
 val record_aux_file : bool ref
 
-(* Flag set when the test-suite is called. Its only effect to display
-   verbose information for `Fail` *)
-val test_mode : bool ref
-
 (** Async-related flags *)
 val async_proofs_worker_id : string ref
 val async_proofs_is_worker : unit -> bool
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index abfda07426..bbccae8edb 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -457,7 +457,7 @@ let parse_args ~help ~init arglist : t * string list =
     |"-batch" ->
       Flags.quiet := true;
       { oval with batch = true }
-    |"-test-mode" -> Flags.test_mode := true; oval
+    |"-test-mode" -> Vernacentries.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
     |"-boot" ->
       warn_deprecated_boot ();
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 11b64a5247..d9d824ad98 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2377,6 +2377,8 @@ let locate_if_not_already ?loc (e, info) =
 exception HasNotFailed
 exception HasFailed of Pp.t
 
+let test_mode = ref false
+
 (* XXX STATE: this type hints that restoring the state should be the
    caller's responsibility *)
 let with_fail st b f =
@@ -2402,7 +2404,7 @@ let with_fail st b f =
       | HasNotFailed ->
           user_err ~hdr:"Fail" (str "The command has not failed!")
       | HasFailed msg ->
-          if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info
+          if not !Flags.quiet || !test_mode then Feedback.msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 4fbd3849b0..f43cec48e9 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -41,3 +41,7 @@ val command_focus : unit Proof.focus_kind
 
 val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
   Evd.evar_map * Redexpr.red_expr) Hook.t
+
+(* Flag set when the test-suite is called. Its only effect to display
+   verbose information for `Fail` *)
+val test_mode : bool ref