1 files changed, 17 insertions, 23 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index db548ec326..d2dcbd92aa 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
@@ -43,7 +43,7 @@ let is_alias_of_already_visible_name sp = function
       false
 
 let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
-  if not (is_alias_of_already_visible_name sp pat) then begin
+  if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
     Nametab.push_syndef (Nametab.Exactly i) sp kn;
     match onlyparse with
     | None ->
@@ -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 msg_warning 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) }