diff options
| author | Maxime Dénès | 2017-09-15 09:41:43 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-15 09:41:43 +0200 |
| commit | 22faf0ba8ca626903ee0f0988953e91252eeab74 (patch) | |
| tree | 7100610d8bac8a1d44d471d3e70d290a30b960a1 | |
| parent | 5c12b6833540f1895d1bb198971d3527e70dce8b (diff) | |
| parent | 73d577c2d959de975415f2807df6a22fa392d335 (diff) | |
Merge PR #938: [parsing] Remove hacks for reduced Prelude.
| -rw-r--r-- | parsing/g_vernac.ml4 | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 560a9a7578..b9a162bec5 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 |