diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 16 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 5 |
4 files changed, 4 insertions, 23 deletions
@@ -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; |