Revert "A new infrastructure for warnings."

This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.

I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.

4 files changed, 35 insertions, 28 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 74de6f67ff..5c5a900fba 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1166,6 +1166,10 @@ 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 :
@@ -1738,6 +1742,7 @@ 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 b0a2192004..e777e5c24e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -190,8 +190,7 @@ let declare_delimiters scope key =
     | None -> scope_map := String.Map.add scope newsc !scope_map
     | Some oldkey when String.equal oldkey key -> ()
     | Some oldkey ->
-        (** FIXME: implement multikey scopes? *)
-	Flags.if_verbose Feedback.msg_info
+	Feedback.msg_warning
 	  (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
 	scope_map := String.Map.add scope newsc !scope_map
   end;
@@ -199,7 +198,7 @@ let declare_delimiters scope key =
     let oldscope = String.Map.find key !delimiters_map in
     if String.equal oldscope scope then ()
     else begin
-      Flags.if_verbose Feedback.msg_info (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
+      Feedback.msg_warning (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
@@ -208,7 +207,7 @@ let remove_delimiters scope =
   let sc = find_scope scope in
   let newsc = { sc with delimiters = None } in
   match sc.delimiters with
-    | None -> Errors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
+    | None -> Feedback.msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
     | Some key ->
        scope_map := String.Map.add scope newsc !scope_map;
        try
@@ -387,12 +386,6 @@ 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
@@ -400,8 +393,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 _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
-    warn_notation_overridden (ntn,which_scope)
+    | Some _ -> str " in scope " ++ str scope in
+    Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
   in
   let notdata = {
     not_interp = pat;
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 7170fd14a5..9a1483b105 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -84,26 +84,23 @@ 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 allow_compat_notations = ref true
+let verbose_compat_notations = ref false
 
 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
-    | _ -> 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
+  !verbose_compat_notations || not !allow_compat_notations
 
 let verbose_compat kn def = function
   | Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
-     warn_compatibility_notation (kn, def, 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)
   | _ -> ()
 
 let search_syntactic_definition kn =
@@ -122,3 +119,12 @@ 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 aa2c9c3c1b..7a1c9c5cb4 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -18,5 +18,8 @@ val declare_syntactic_definition : bool -> Id.t ->
 
 val search_syntactic_definition : kernel_name -> syndef_interpretation
 
-(** Option concerning verbose display of compatibility notations  *)
+(** Options concerning verbose display of compatibility notations
+    or their deactivation *)
+
 val set_verbose_compat_notations : bool -> unit
+val set_compat_notations : bool -> unit