Adding a warning in case a notation is used neither for parsing nor printing.

1 files changed, 24 insertions, 14 deletions

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 875a69f687..8ce59c40c3 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1412,8 +1412,7 @@ type notation_obj = {
   notobj_scope : scope_name option;
   notobj_interp : interpretation;
   notobj_coercion : entry_coercion_kind option;
-  notobj_onlyparse : bool;
-  notobj_onlyprint : bool;
+  notobj_use : notation_use option;
   notobj_deprecation : Deprecation.t option;
   notobj_notation : notation * notation_location;
   notobj_specific_pp_rules : syntax_printing_extension option;
@@ -1439,20 +1438,17 @@ let open_notation i (_, nobj) =
     let pat = nobj.notobj_interp in
     let deprecation = nobj.notobj_deprecation in
     let scope = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
-    let use = match nobj.notobj_onlyparse, nobj.notobj_onlyprint with
-      | false, false -> ParsingAndPrinting
-      | true, false -> OnlyParsing
-      | false, true -> OnlyPrinting
-      | true, true -> assert false in
     (* Declare the notation *)
-    Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation;
+    (match nobj.notobj_use with
+    | Some use -> Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation
+    | None -> ());
     (* Declare specific format if any *)
-    match nobj.notobj_specific_pp_rules with
+    (match nobj.notobj_specific_pp_rules with
     | Some pp_sy ->
       if specific_format_to_declare (scope,ntn) pp_sy then
         Ppextend.declare_specific_notation_printing_rules
           (scope,ntn) ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
-    | None -> ()
+    | None -> ())
   end
 
 let cache_notation o =
@@ -1582,6 +1578,20 @@ let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in
     synext_extra  = sd.extra;
   }
 
+let warn_unused_interpretation =
+  CWarnings.create ~name:"unused-notation" ~category:"parsing"
+         (fun b ->
+          strbrk "interpretation is used neither for printing nor for parsing, " ++
+          (if b then strbrk "the declaration could be replaced by \"Reserved Notation\"."
+          else strbrk "the declaration could be removed."))
+
+let make_use reserved onlyparse onlyprint =
+  match onlyparse, onlyprint with
+  | false, false -> Some ParsingAndPrinting
+  | true, false -> Some OnlyParsing
+  | false, true -> Some OnlyPrinting
+  | true, true -> warn_unused_interpretation reserved; None
+
 (**********************************************************************)
 (* Main functions about notations                                     *)
 
@@ -1613,14 +1623,14 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
   let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in
   let notation, location = sd.info in
+  let use = make_use true onlyparse sd.only_printing in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
     notobj_interp = (List.map_filter map i_vars, ac);
     (* Order is important here! *)
-    notobj_onlyparse = onlyparse;
+    notobj_use = use;
     notobj_coercion = coe;
-    notobj_onlyprint = sd.only_printing;
     notobj_deprecation = sd.deprecation;
     notobj_notation = (notation, location);
     notobj_specific_pp_rules = sy_pp_rules;
@@ -1656,14 +1666,14 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
   let interp = make_interpretation_vars recvars plevel acvars (List.combine mainvars i_typs) in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
   let onlyparse,coe = printability level i_typs onlyparse reversibility ac in
+  let use = make_use false onlyparse onlyprint in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
     notobj_interp = (List.map_filter map i_vars, ac);
     (* Order is important here! *)
-    notobj_onlyparse = onlyparse;
+    notobj_use = use;
     notobj_coercion = coe;
-    notobj_onlyprint = onlyprint;
     notobj_deprecation = deprecation;
     notobj_notation = df';
     notobj_specific_pp_rules = pp_sy;