From 88fe0bcf86ad6cb95ffacfcd37f51fa3ae2da4fc Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Nov 2019 15:50:39 +0100 Subject: Remove deprecated compat modifier of Notation / Infix commands. And simplify a lot the compatibility infrastructure following this. Update dev/tools/update-compat.py Remove much complexity. Co-authored-by: Jason Gross --- dev/tools/update-compat.py | 109 +++------------------ doc/changelog/03-notations/11113-remove-compat.rst | 4 + lib/flags.ml | 30 ------ lib/flags.mli | 9 +- test-suite/success/NotationDeprecation.v | 24 ----- toplevel/coqargs.ml | 23 +++-- vernac/g_vernac.mlg | 23 +---- vernac/metasyntax.ml | 28 +----- vernac/metasyntax.mli | 2 +- vernac/ppvernac.ml | 9 +- vernac/vernacentries.ml | 4 +- vernac/vernacexpr.ml | 3 +- 12 files changed, 39 insertions(+), 229 deletions(-) create mode 100644 doc/changelog/03-notations/11113-remove-compat.rst diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index 7312c2a5af..ddb0362186 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -15,10 +15,8 @@ from io import open # [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) # with the deleted file. # - Remove any notations in the standard library which have `compat "U.U"`. -# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by -# bumping all the version numbers by one, and update the interpretations -# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and -# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). +# - Update the function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) +# by bumping all the version numbers by one. # # - Remove the file # [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v). @@ -38,10 +36,8 @@ from io import open # - Update # [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) # with the added file. -# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by -# bumping all the version numbers by one, and update the interpretations -# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and -# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). +# - Update the function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) +# by bumping all the version numbers by one. # - Update the files # [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), # [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), @@ -70,10 +66,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2 RELEASE_NUMBER_OF_OLD_VERSIONS = 2 MASTER_NUMBER_OF_OLD_VERSIONS = 3 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n' -FLAGS_MLI_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.mli') -FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml') COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') -G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) @@ -248,118 +241,38 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar contents = contents.replace(header, '%s\n%s' % (header, line)) update_file(contents, compat_path, exn_string=('Compat file %%s is missing line %s' % line), assert_unchanged=assert_unchanged, **args) -def update_compat_versions_type_line(new_versions, contents, relpath): - compat_version_string = ' | '.join(['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']) - new_compat_line = 'type compat_version = %s' % compat_version_string - new_contents = re.sub(r'^type compat_version = .*$', new_compat_line, contents, flags=re.MULTILINE) - if new_compat_line not in new_contents: - raise Exception("Could not find 'type compat_version =' in %s" % relpath) - return new_contents - -def update_version_compare(new_versions, contents, relpath): - first_line = 'let version_compare v1 v2 = match v1, v2 with' - new_lines = [first_line] - for v in new_versions[:-1]: - V = 'V%s_%s' % tuple(v.split('.')) - new_lines.append(' | %s, %s -> 0' % (V, V)) - new_lines.append(' | %s, _ -> -1' % V) - new_lines.append(' | _, %s -> 1' % V) - new_lines.append(' | Current, Current -> 0') - new_lines = '\n'.join(new_lines) - new_contents = re.sub(first_line + '.*' + 'Current, Current -> 0', new_lines, contents, flags=re.DOTALL|re.MULTILINE) - if new_lines not in new_contents: - raise Exception('Could not find version_compare in %s' % relpath) - return new_contents - -def update_pr_version(new_versions, contents, relpath): - first_line = 'let pr_version = function' - new_lines = [first_line] - for v in new_versions[:-1]: - V = 'V%s_%s' % tuple(v.split('.')) - new_lines.append(' | %s -> "%s"' % (V, v)) - new_lines.append(' | Current -> "current"') - new_lines = '\n'.join(new_lines) - new_contents = re.sub(first_line + '.*' + 'Current -> "current"', new_lines, contents, flags=re.DOTALL|re.MULTILINE) - if new_lines not in new_contents: - raise Exception('Could not find pr_version in %s' % relpath) - return new_contents - -def update_add_compat_require(new_versions, contents, relpath): - first_line = 'let add_compat_require opts v =' - new_lines = [first_line, ' match v with'] - for v in new_versions[:-1]: - V = 'V%s_%s' % tuple(v.split('.')) - new_lines.append(' | Flags.%s -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % (V, version_name_to_compat_name(v, ext=''))) - new_lines.append(' | Flags.Current -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % version_name_to_compat_name(new_versions[-1], ext='')) - new_lines = '\n'.join(new_lines) - new_contents = re.sub(first_line + '.*' + 'Flags.Current -> add_vo_require opts "Coq.Compat.[^"]+" None .Some false.', new_lines, contents, flags=re.DOTALL|re.MULTILINE) - if new_lines not in new_contents: - raise Exception('Could not find add_compat_require in %s' % relpath) - return new_contents - -def update_parse_compat_version(new_versions, contents, relpath, **args): +def update_get_compat_file(new_versions, contents, relpath): line_count = 3 # 1 for the first line, 1 for the invalid flags, and 1 for Current - first_line = 'let parse_compat_version = let open Flags in function' + first_line = 'let get_compat_file = function' split_contents = contents[contents.index(first_line):].split('\n') while True: cur_line = split_contents[:line_count][-1] if re.match(r'^ \| \([0-9 "\.\|]*\) as s ->$', cur_line) is not None: break - elif re.match(r'^ \| "[0-9\.]*" -> V[0-9_]*$', cur_line) is not None: + elif re.match(r'^ \| "[0-9\.]*" -> "Coq.Compat.Coq[0-9]*"$', cur_line) is not None: line_count += 1 else: - raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line))) + raise Exception('Could not recognize line %d of get_compat_file in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line))) old_function_lines = split_contents[:line_count] all_versions = re.findall(r'"([0-9\.]+)"', ''.join(old_function_lines)) invalid_versions = tuple(i for i in all_versions if i not in new_versions) new_function_lines = [first_line] - for v, V in reversed(list(zip(new_versions, ['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']))): + for v, V in reversed(list(zip(new_versions, ['"Coq.Compat.Coq%s%s"' % tuple(v.split('.')) for v in new_versions]))): new_function_lines.append(' | "%s" -> %s' % (v, V)) new_function_lines.append(' | (%s) as s ->' % ' | '.join('"%s"' % v for v in invalid_versions)) new_lines = '\n'.join(new_function_lines) new_contents = contents.replace('\n'.join(old_function_lines), new_lines) if new_lines not in new_contents: - raise Exception('Could not find parse_compat_version in %s' % relpath) + raise Exception('Could not find get_compat_file in %s' % relpath) return new_contents -def check_no_old_versions(old_versions, new_versions, contents, relpath): - for v in old_versions: - if v not in new_versions: - V = 'V%s_%s' % tuple(v.split('.')) - if V in contents: - raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath)) - -def update_flags_mli(old_versions, new_versions, **args): - contents = get_file(FLAGS_MLI_PATH) - new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH)) - check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH)) - update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args) - -def update_flags_ml(old_versions, new_versions, **args): - contents = get_file(FLAGS_ML_PATH) - new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) - new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) - new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) - check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) - update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args) - def update_coqargs_ml(old_versions, new_versions, **args): contents = get_file(COQARGS_ML_PATH) - new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH)) - check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH)) + new_contents = update_get_compat_file(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH)) update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args) -def update_g_vernac(old_versions, new_versions, **args): - contents = get_file(G_VERNAC_PATH) - new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args) - check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH)) - update_if_changed(contents, new_contents, G_VERNAC_PATH, **args) - def update_flags(old_versions, new_versions, **args): - update_flags_mli(old_versions, new_versions, **args) - update_flags_ml(old_versions, new_versions, **args) update_coqargs_ml(old_versions, new_versions, **args) - update_g_vernac(old_versions, new_versions, **args) def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, test_suite_outdated_paths=tuple(), **args): assert(len(new_versions) == len(test_suite_paths)) diff --git a/doc/changelog/03-notations/11113-remove-compat.rst b/doc/changelog/03-notations/11113-remove-compat.rst new file mode 100644 index 0000000000..8c71d70cda --- /dev/null +++ b/doc/changelog/03-notations/11113-remove-compat.rst @@ -0,0 +1,4 @@ +- Removed deprecated ``compat`` modifier of :cmd:`Notation` + and :cmd:`Infix` commands + (`#11113 `_, + by Théo Zimmermann, with help from Jason Gross). diff --git a/lib/flags.ml b/lib/flags.ml index 27ca8e9596..b87ba46634 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -57,36 +57,6 @@ let raw_print = ref false let we_are_parsing = ref false -(* Compatibility mode *) - -(* Current means no particular compatibility consideration. - For correct comparisons, this constructor should remain the last one. *) - -type compat_version = V8_9 | V8_10 | V8_11 | Current - -let compat_version = ref Current - -let version_compare v1 v2 = match v1, v2 with - | V8_9, V8_9 -> 0 - | V8_9, _ -> -1 - | _, V8_9 -> 1 - | V8_10, V8_10 -> 0 - | V8_10, _ -> -1 - | _, V8_10 -> 1 - | V8_11, V8_11 -> 0 - | V8_11, _ -> -1 - | _, V8_11 -> 1 - | Current, Current -> 0 - -let version_strictly_greater v = version_compare !compat_version v > 0 -let version_less_or_equal v = not (version_strictly_greater v) - -let pr_version = function - | V8_9 -> "8.9" - | V8_10 -> "8.10" - | V8_11 -> "8.11" - | Current -> "current" - (* Translate *) let beautify = ref false let beautify_file = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 36a996401d..86a922847f 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -14,7 +14,7 @@ This file is own its way to deprecation in favor of a purely functional state, but meanwhile it will contain options that are - truly global to the system such as [compat] or [debug] + truly global to the system such as [debug] If you are thinking about adding a global flag, well, just don't. First of all, options make testins exponentially more @@ -52,13 +52,6 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -type compat_version = V8_9 | V8_10 | V8_11 | Current -val compat_version : compat_version ref -val version_compare : compat_version -> compat_version -> int -val version_strictly_greater : compat_version -> bool -val version_less_or_equal : compat_version -> bool -val pr_version : compat_version -> string - (* Beautify command line flags, should move to printing? *) val beautify : bool ref val beautify_file : bool ref diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v index 96814a1b97..60d40d3d12 100644 --- a/test-suite/success/NotationDeprecation.v +++ b/test-suite/success/NotationDeprecation.v @@ -3,19 +3,11 @@ Module Syndefs. #[deprecated(since = "8.9", note = "Do not use.")] Notation foo := Prop. -Notation bar := Prop (compat "8.9"). - -Fail -#[deprecated(since = "8.9", note = "Do not use.")] -Notation zar := Prop (compat "8.9"). - Check foo. -Check bar. Set Warnings "+deprecated". Fail Check foo. -Fail Check bar. End Syndefs. @@ -24,19 +16,11 @@ Module Notations. #[deprecated(since = "8.9", note = "Do not use.")] Notation "!!" := Prop. -Notation "##" := Prop (compat "8.9"). - -Fail -#[deprecated(since = "8.9", note = "Do not use.")] -Notation "**" := Prop (compat "8.9"). - Check !!. -Check ##. Set Warnings "+deprecated". Fail Check !!. -Fail Check ##. End Notations. @@ -45,18 +29,10 @@ Module Infix. #[deprecated(since = "8.9", note = "Do not use.")] Infix "!!" := plus (at level 1). -Infix "##" := plus (at level 1, compat "8.9"). - -Fail -#[deprecated(since = "8.9", note = "Do not use.")] -Infix "**" := plus (at level 1, compat "8.9"). - Check (_ !! _). -Check (_ ## _). Set Warnings "+deprecated". Fail Check (_ !! _). -Fail Check (_ ## _). End Infix. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index e3116550d9..5326ce6114 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -174,13 +174,6 @@ let add_vo_include opts unix_path coq_path implicit = let add_vo_require opts d p export = { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }} -let add_compat_require opts v = - match v with - | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) - | Flags.V8_10 -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) - | Flags.V8_11 -> add_vo_require opts "Coq.Compat.Coq811" None (Some false) - | Flags.Current -> add_vo_require opts "Coq.Compat.Coq812" None (Some false) - let add_load_vernacular opts verb s = { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }} @@ -274,6 +267,18 @@ let get_native_name s = Nativelib.output_dir; Library.native_name_from_filename s] with _ -> "" +let get_compat_file = function + | "8.12" -> "Coq.Compat.Coq812" + | "8.11" -> "Coq.Compat.Coq811" + | "8.10" -> "Coq.Compat.Coq810" + | "8.9" -> "Coq.Compat.Coq89" + | ("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_file" + Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") + | s -> + CErrors.user_err ~hdr:"get_compat_file" + Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") + let to_opt_key = Str.(split (regexp " +")) let parse_option_set opt = @@ -379,9 +384,7 @@ let parse_args ~help ~init arglist : t * string list = |"-worker-id" -> set_worker_id opt (next ()); oval |"-compat" -> - let v = G_vernac.parse_compat_version (next ()) in - Flags.compat_version := v; - add_compat_require oval v + add_vo_require oval (get_compat_file (next ())) None (Some false) |"-exclude-dir" -> System.exclude_directory (next ()); oval 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 bb55cd5114..1bf34f2922 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 = -- cgit v1.2.3