Remove the Set Verbose Compat option and turn the warning on by default.

These warnings can now be configured like any other, so we don't need
a specific option anymore.

4 files changed, 4 insertions, 23 deletions

diff --git a/CHANGES b/CHANGES
index a9ce5260a7..6ea680153d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -100,6 +100,9 @@ Tools
 - Setting [Printing Dependent Evars Line] can be unset to disable the
   computation associated with printing the "dependent evars: " line in
   -emacs mode
+- Removed the -verbose-compat-notations flag and the corresponding Set
+  Verbose Compat vernacular, since these warnings can now be silenced or
+  turned into errors using "-w".
 
 Changes from V8.5pl2 to V8.5pl3
 ===============================
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index d2dcbd92aa..b2b82cce37 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -84,11 +84,6 @@ let declare_syntactic_definition local id onlyparse pat =
 
 let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
 
-let verbose_compat_notations = ref true
-
-let is_verbose_compat () =
-  !verbose_compat_notations
-
 let pr_compat_warning (kn, def, v) =
   let pp_def = match def with
     | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r
@@ -102,7 +97,7 @@ let warn_compatibility_notation =
                    ~category:"deprecated" pr_compat_warning
 
 let verbose_compat kn def = function
-  | Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
+  | Some v when Flags.version_strictly_greater v ->
      warn_compatibility_notation (kn, def, v)
   | _ -> ()
 
@@ -113,12 +108,3 @@ let search_syntactic_definition kn =
   def
 
 open Goptions
-
-let set_verbose_compat_notations =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "verbose compatibility notations";
-      optkey   = ["Verbose";"Compat";"Notations"];
-      optread  = (fun () -> !verbose_compat_notations);
-      optwrite = ((:=) verbose_compat_notations) }
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index aa2c9c3c1b..55e2848e69 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -17,6 +17,3 @@ val declare_syntactic_definition : bool -> Id.t ->
   Flags.compat_version option -> syndef_interpretation -> unit
 
 val search_syntactic_definition : kernel_name -> syndef_interpretation
-
-(** Option concerning verbose display of compatibility notations  *)
-val set_verbose_compat_notations : bool -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 47d433d790..cf0efca69d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -332,7 +332,6 @@ let error_missing_arg s =
 let filter_opts = ref false
 let exitcode () = if !filter_opts then 2 else 0
 
-let verb_compat_ntn = ref false
 let no_compat_ntn = ref false
 
 let print_where = ref false
@@ -576,7 +575,6 @@ let parse_args arglist =
     |"-unicode" -> add_require "Utf8_core"
     |"-v"|"--version" -> Usage.version (exitcode ())
     |"--print-version" -> Usage.machine_readable_version (exitcode ())
-    |"-verbose-compat-notations" -> verb_compat_ntn := true
     |"-where" -> print_where := true
     |"-xml" -> Flags.xml_export := true
 
@@ -637,9 +635,6 @@ let init_toplevel arglist =
       inputstate ();
       Mltop.init_known_plugins ();
       engage ();
-      (* Be careful to set these variables after the inputstate *)
-      Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
-(*       Syntax_def.set_compat_notations (not !no_compat_ntn); FIXME *)
       if (not !batch_mode || List.is_empty !compile_list)
          && Global.env_is_initial ()
       then Option.iter Declaremods.start_library !toplevel_name;