diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 5 | ||||
| -rw-r--r-- | interp/notation.ml | 17 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 36 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 5 |
4 files changed, 28 insertions, 35 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5c5a900fb..74de6f67f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1166,10 +1166,6 @@ let alias_of als = match als.alias_ids with | [] -> Anonymous | id :: _ -> Name id -let message_redundant_alias id1 id2 = - Feedback.msg_warning - (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2) - (** {6 Expanding notations } @returns a raw_case_pattern_expr : @@ -1742,7 +1738,6 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in List.map (fun (asubst,pl) -> let rhs = replace_vars_constr_expr asubst rhs in - Id.Map.iter message_redundant_alias asubst; let rhs' = intern {env with ids = env_ids} rhs in (loc,eqn_ids,pl,rhs')) pll diff --git a/interp/notation.ml b/interp/notation.ml index e777e5c24..b0a219200 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -190,7 +190,8 @@ let declare_delimiters scope key = | None -> scope_map := String.Map.add scope newsc !scope_map | Some oldkey when String.equal oldkey key -> () | Some oldkey -> - Feedback.msg_warning + (** FIXME: implement multikey scopes? *) + Flags.if_verbose Feedback.msg_info (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope); scope_map := String.Map.add scope newsc !scope_map end; @@ -198,7 +199,7 @@ let declare_delimiters scope key = let oldscope = String.Map.find key !delimiters_map in if String.equal oldscope scope then () else begin - Feedback.msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope); + Flags.if_verbose Feedback.msg_info (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope); delimiters_map := String.Map.add key scope !delimiters_map end with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map @@ -207,7 +208,7 @@ let remove_delimiters scope = let sc = find_scope scope in let newsc = { sc with delimiters = None } in match sc.delimiters with - | None -> Feedback.msg_warning (str "No bound key for scope " ++ str scope ++ str ".") + | None -> Errors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".") | Some key -> scope_map := String.Map.add scope newsc !scope_map; try @@ -386,6 +387,12 @@ let level_of_notation ntn = (* The mapping between notations and their interpretation *) +let warn_notation_overridden = + CWarnings.create ~name:"notation-overridden" ~category:"parsing" + (fun (ntn,which_scope) -> + str "Notation" ++ spc () ++ str ntn ++ spc () + ++ strbrk "was already used" ++ which_scope) + let declare_notation_interpretation ntn scopt pat df ~onlyprint = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in @@ -393,8 +400,8 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = if String.Map.mem ntn sc.notations then let which_scope = match scopt with | None -> mt () - | Some _ -> str " in scope " ++ str scope in - Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope) + | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in + warn_notation_overridden (ntn,which_scope) in let notdata = { not_interp = pat; diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 9a1483b10..7170fd14a 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -84,23 +84,26 @@ let declare_syntactic_definition local id onlyparse pat = let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) -let allow_compat_notations = ref true -let verbose_compat_notations = ref false +let verbose_compat_notations = ref true let is_verbose_compat () = - !verbose_compat_notations || not !allow_compat_notations + !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 + | _ -> strbrk " is a compatibility notation" + in + let since = strbrk " since Coq > " ++ str (Flags.pr_version v) ++ str "." in + pr_syndef kn ++ pp_def ++ since + +let warn_compatibility_notation = + CWarnings.create ~name:"compatibility-notation" + ~category:"deprecated" pr_compat_warning let verbose_compat kn def = function | Some v when is_verbose_compat () && Flags.version_strictly_greater v -> - let act = - if !verbose_compat_notations then Feedback.msg_warning ?loc:None else errorlabstrm "" - in - let pp_def = match def with - | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r - | _ -> str " is a compatibility notation" - in - let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in - act (pr_syndef kn ++ pp_def ++ since) + warn_compatibility_notation (kn, def, v) | _ -> () let search_syntactic_definition kn = @@ -119,12 +122,3 @@ let set_verbose_compat_notations = optkey = ["Verbose";"Compat";"Notations"]; optread = (fun () -> !verbose_compat_notations); optwrite = ((:=) verbose_compat_notations) } - -let set_compat_notations = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "accept compatibility notations"; - optkey = ["Compat"; "Notations"]; - optread = (fun () -> !allow_compat_notations); - optwrite = ((:=) allow_compat_notations) } diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 7a1c9c5cb..aa2c9c3c1 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -18,8 +18,5 @@ val declare_syntactic_definition : bool -> Id.t -> val search_syntactic_definition : kernel_name -> syndef_interpretation -(** Options concerning verbose display of compatibility notations - or their deactivation *) - +(** Option concerning verbose display of compatibility notations *) val set_verbose_compat_notations : bool -> unit -val set_compat_notations : bool -> unit |