diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-31 14:06:02 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-31 14:06:02 +0200 |
commit | 1c55826018c5f07ee25b5771e59fe0389293cb62 (patch) | |
tree | 7e9f641d39a29e5848c4e8bc90b9702dc793c899 /parsing | |
parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) |
[general] Remove spurious dependency of highparsing on toplevel.
`G_vernac` was depending on `toplevel` just for parsing the compat
number information. IMHO this was not the right place, so I have moved
the parsing bits to parsing and updated the files.
This allows to finally separate the `toplevel` from Coq, which avoids
linking it in alternative toplevels.
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/g_vernac.ml4 | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3d29fca77..99c8b1dbf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -51,6 +51,19 @@ let make_bullet s = | '*' -> Star n | _ -> assert false +let parse_compat_version ?(allow_old = true) = let open Flags in function + | "8.8" -> Current + | "8.7" -> V8_7 + | "8.6" -> V8_6 + | "8.5" -> V8_5 + | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + if allow_old then VOld else + 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 "\".") + let extraction_err ~loc = if not (Mltop.module_is_known "extraction_plugin") then CErrors.user_err ~loc (str "Please do first a Require Extraction.") @@ -1163,7 +1176,7 @@ GEXTEND Gram [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> Some Flags.Current | "("; IDENT "compat"; s = STRING; ")" -> - Some (Coqinit.get_compat_version s) + Some (parse_compat_version s) | -> None ] ] ; obsolete_locality: @@ -1181,7 +1194,7 @@ GEXTEND Gram | IDENT "only"; IDENT "printing" -> SetOnlyPrinting | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> - SetCompatVersion (Coqinit.get_compat_version s) + SetCompatVersion (parse_compat_version s) | IDENT "format"; s1 = [s = STRING -> Loc.tag ~loc:!@loc s]; s2 = OPT [s = STRING -> Loc.tag ~loc:!@loc s] -> begin match s1, s2 with |