Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.

Reviewed-by: JasonGross
Reviewed-by: ejgallego
Reviewed-by: maximedenes

6 files changed, 10 insertions, 59 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5f088379ca..436648c163 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -62,18 +62,6 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
-let parse_compat_version = let open Flags in function
-  | "8.12" -> Current
-  | "8.11" -> V8_11
-  | "8.10" -> V8_10
-  | "8.9" -> V8_9
-  | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
-    CErrors.user_err ~hdr:"get_compat_version"
-      Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
-  | s ->
-    CErrors.user_err ~hdr:"get_compat_version"
-      Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
-
 (* For now we just keep the top-level location of the whole
    vernacular, that is to say, including attributes and control flags;
    this is not very convenient for advanced clients tho, so in the
@@ -1192,7 +1180,7 @@ GRAMMAR EXTEND Gram
      | IDENT "Notation"; id = identref;
          idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
            { VernacSyntacticDefinition
-             (id,(idl,c),b) }
+             (id,(idl,c),{ onlyparsing = b }) }
      | IDENT "Notation"; s = lstring; ":=";
          c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ];
@@ -1216,11 +1204,8 @@ GRAMMAR EXTEND Gram
   ] ]
   ;
   only_parsing:
-    [ [ "("; IDENT "only"; IDENT "parsing"; ")" ->
-         { Some Flags.Current }
-      | "("; IDENT "compat"; s = STRING; ")" ->
-         { Some (parse_compat_version s) }
-      | -> { None } ] ]
+    [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> { true }
+      | -> { false } ] ]
   ;
   level:
     [ [ IDENT "level"; n = natural -> { NumLevel n }
@@ -1236,8 +1221,6 @@ GRAMMAR EXTEND Gram
       | IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA }
       | IDENT "only"; IDENT "printing" -> { SetOnlyPrinting }
       | IDENT "only"; IDENT "parsing" -> { SetOnlyParsing }
-      | IDENT "compat"; s = STRING ->
-        { SetCompatVersion (parse_compat_version s) }
       | IDENT "format"; s1 = [s = STRING -> { CAst.make ~loc s } ];
                         s2 = OPT [s = STRING -> { CAst.make ~loc s } ] ->
           { begin match s1, s2 with
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index fd57901acd..e23522da9e 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -805,7 +805,6 @@ type notation_modifier = {
   (* common to syn_data below *)
   only_parsing  : bool;
   only_printing : bool;
-  compat        : Flags.compat_version option;
   format        : lstring option;
   extra         : (string * string) list;
 }
@@ -818,7 +817,6 @@ let default = {
   subtyps       = [];
   only_parsing  = false;
   only_printing = false;
-  compat        = None;
   format        = None;
   extra         = [];
 }
@@ -877,8 +875,6 @@ let interp_modifiers modl = let open NotationMods in
         interp subtyps { acc with only_parsing = true; } l
     | SetOnlyPrinting :: l ->
         interp subtyps { acc with only_printing = true; } l
-    | SetCompatVersion v :: l ->
-        interp subtyps { acc with compat = Some v; } l
     | SetFormat ("text",s) :: l ->
         if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
         interp subtyps { acc with format = Some s; } l
@@ -916,7 +912,6 @@ let check_binder_type recvars etyps =
 let not_a_syntax_modifier = function
 | SetOnlyParsing -> true
 | SetOnlyPrinting -> true
-| SetCompatVersion _ -> true
 | _ -> false
 
 let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods
@@ -1213,32 +1208,12 @@ let check_locality_compatibility local custom i_typs =
                     strbrk " which is local."))
       (List.uniquize allcustoms)
 
-let warn_deprecated_compat =
-  CWarnings.create ~name:"deprecated-compat" ~category:"deprecated"
-    (fun () -> Pp.(str"The \"compat\" modifier is deprecated." ++ spc () ++
-                   str"Please use the \"deprecated\" attributed instead."))
-
-(* Returns the new deprecation and the onlyparsing status. This should be
-removed together with the compat syntax modifier. *)
-let merge_compat_deprecation compat deprecation =
-  match compat, deprecation with
-  | Some Flags.Current, _ -> deprecation, true
-  | Some _, Some _ ->
-    CErrors.user_err Pp.(str"The \"compat\" modifier cannot be used with the \"deprecated\" attribute."
-                        ++ spc () ++ str"Please use only the latter.")
-  | Some v, None ->
-    warn_deprecated_compat ();
-    Some (Deprecation.make ~since:(Flags.pr_version v) ()), true
-  | None, Some _ -> deprecation, true
-  | None, None -> deprecation, false
-
 let compute_syntax_data ~local deprecation df modifiers =
   let open SynData in
   let open NotationMods in
   let mods = interp_modifiers modifiers in
   let onlyprint = mods.only_printing in
   let onlyparse = mods.only_parsing in
-  let deprecation, _ = merge_compat_deprecation mods.compat deprecation in
   if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
   let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
   let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
@@ -1659,7 +1634,7 @@ let try_interp_name_alias = function
   | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
   | _ -> raise Not_found
 
-let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
+let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
   let vars,reversibility,pat =
     try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
     with Not_found ->
@@ -1673,7 +1648,6 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
       let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
       List.map map vars, reversibility, pat
   in
-  let deprecation, onlyparsing = merge_compat_deprecation compat deprecation in
   let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
   Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
 
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 44e08c4819..e3e733a4b7 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -52,7 +52,7 @@ val add_syntax_extension :
 (** Add a syntactic definition (as in "Notation f := ...") *)
 
 val add_syntactic_definition : local:bool -> Deprecation.t option -> env ->
-  Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit
+  Id.t -> Id.t list * constr_expr -> onlyparsing_flag -> unit
 
 (** Print the Camlp5 state of a grammar *)
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1aa9a4e0f5..1742027076 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -412,7 +412,6 @@ let string_of_theorem_kind = let open Decls in function
     | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ
     | SetOnlyPrinting -> keyword "only printing"
     | SetOnlyParsing -> keyword "only parsing"
-    | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
     | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s
     | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s
 
@@ -1059,16 +1058,12 @@ let string_of_definition_object_kind = let open Decls in function
         )
       | VernacHints (dbnames,h) ->
         return (pr_hints dbnames h (pr_constr env sigma) (pr_constr_pattern_expr env sigma))
-      | VernacSyntacticDefinition (id,(ids,c),compat) ->
+      | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) ->
         return (
           hov 2
             (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
                prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
-               pr_syntax_modifiers
-               (match compat with
-                | None -> []
-                | Some Flags.Current -> [SetOnlyParsing]
-                | Some v -> [SetCompatVersion v]))
+               pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
         )
       | VernacArguments (q, args, more_implicits, mods) ->
         return (
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index de7695791f..e4965614d8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1206,10 +1206,10 @@ let vernac_hints ~atts dbnames h =
   let local = enforce_module_locality local in
   Hints.add_hints ~local dbnames (Hints.interp_hints ~poly h)
 
-let vernac_syntactic_definition ~atts lid x compat =
+let vernac_syntactic_definition ~atts lid x only_parsing =
   let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
   Dumpglob.dump_definition lid false "syndef";
-  Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat
+  Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x only_parsing
 
 let default_env () = {
   Notation_term.ninterp_var_type = Id.Map.empty;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index bec6a0d2bb..32ff8b8fb2 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -105,7 +105,7 @@ type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
 type export_flag    = bool (* true = Export;        false = Import         *)
 type inductive_flag = Declarations.recursivity_kind
-type onlyparsing_flag = Flags.compat_version option
+type onlyparsing_flag = { onlyparsing : bool }
  (* Some v = Parse only;  None = Print also.
     If v<>Current, it contains the name of the coq version
     which this notation is trying to be compatible with *)
@@ -185,7 +185,6 @@ type syntax_modifier =
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
   | SetOnlyParsing
   | SetOnlyPrinting
-  | SetCompatVersion of Flags.compat_version
   | SetFormat of string * lstring
 
 type proof_end =