From d0dda9c419894460de952d4b9342ea6518d24f83 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 6 Oct 2016 11:14:08 +0200 Subject: 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. --- interp/syntax_def.ml | 16 +--------------- interp/syntax_def.mli | 3 --- 2 files changed, 1 insertion(+), 18 deletions(-) (limited to 'interp') diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index d2dcbd92a..b2b82cce3 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 aa2c9c3c1..55e2848e6 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 -- cgit v1.2.3 From d180279aa934dfbb3fd97e707675b55f464f14ef Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 6 Oct 2016 14:02:52 +0200 Subject: Disable compatibility notations warnings. Enablnig them would give a system that tells the user to replace e.g.: le_n_Sn with Nat.le_succ_diag_r lt_S with Nat.lt_lt_succ_r (on other types like R and and positive, the same lemma is called lt_lt_succ) In many cases, the new names will be too painful for intensive users. --- interp/syntax_def.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index b2b82cce3..2523063e6 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -93,8 +93,8 @@ let pr_compat_warning (kn, def, v) = pr_syndef kn ++ pp_def ++ since let warn_compatibility_notation = - CWarnings.create ~name:"compatibility-notation" - ~category:"deprecated" pr_compat_warning + CWarnings.(create ~name:"compatibility-notation" + ~category:"deprecated" ~default:Disabled pr_compat_warning) let verbose_compat kn def = function | Some v when Flags.version_strictly_greater v -> -- cgit v1.2.3