aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-07-31 14:18:25 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-08-29 17:21:57 +0200
commit73d577c2d959de975415f2807df6a22fa392d335 (patch)
tree152922be2f8f646cf2b5ce9ce5fe7979cb60bafe /parsing
parentf1806ab001cfbc9548e607397fc55b9c1be7c25b (diff)
[parsing] Remove hacks for reduced Prelude.
These hacks to warn the users about needed modules are not needed anymore in 8.8, as the proper error message is done in 8.7 already. This helps in avoiding a dependency from parsing to MlTop.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_vernac.ml430
1 files changed, 0 insertions, 30 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 560a9a757..b9a162bec 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -64,20 +64,6 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function
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.")
- else
- (* The right grammar entries should have been loaded.
- We could only end here in case of syntax error. *)
- raise (Stream.Error "unexpected end of command")
-
-let funind_err ~loc =
- if not (Mltop.module_is_known "recdef_plugin") then
- CErrors.user_err ~loc (str "Please do first a Require Import FunInd.")
- else
- raise (Stream.Error "unexpected end of command") (* Same as above... *)
-
GEXTEND Gram
GLOBAL: vernac gallina_ext noedit_mode subprf;
vernac: FIRST
@@ -881,22 +867,6 @@ GEXTEND Gram
| IDENT "DelPath"; dir = ne_string ->
VernacRemoveLoadPath dir
- (* Some plugins are not loaded initially anymore : extraction,
- and funind. To ease this transition toward a mandatory Require,
- we hack here the vernac grammar in order to get customized
- error messages telling what to Require instead of the dreadful
- "Illegal begin of vernac". Normally, these fake grammar entries
- are overloaded later by the grammar extensions in these plugins.
- This code is meant to be removed in a few releases, when this
- transition is considered finished. *)
-
- | IDENT "Extraction" -> extraction_err ~loc:!@loc
- | IDENT "Extract" -> extraction_err ~loc:!@loc
- | IDENT "Recursive"; IDENT "Extraction" -> extraction_err ~loc:!@loc
- | IDENT "Separate"; IDENT "Extraction" -> extraction_err ~loc:!@loc
- | IDENT "Function" -> funind_err ~loc:!@loc
- | IDENT "Functional" -> funind_err ~loc:!@loc
-
(* Type-Checking (pas dans le refman) *)
| "Type"; c = lconstr -> VernacGlobalCheck c