diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:43:50 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:43:50 +0200 |
| commit | c3bc1fda9c5dd1805b23d04f2dee711aeec1f4a1 (patch) | |
| tree | b62cd62e04d2e965ebc2d19da69fb42ad5d0bd3b /parsing | |
| parent | 9326b0466cc04175436dc57cf0283c151b587e54 (diff) | |
| parent | 1c55826018c5f07ee25b5771e59fe0389293cb62 (diff) | |
Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.
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 93a778274..560a9a757 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.") @@ -1168,7 +1181,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: @@ -1186,7 +1199,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 |