Grammar hacks to get nice errors about non-loaded plugins (extr,recdef)

 Since previous commit, some plugins are not loaded initially anymore :
 extraction, 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.

 NB : In a first attempt, a similar trick was tried in g_tactics.ml4 to
 provide customized error message for "functional induction" and "functional
 inversion", but this was leading to anomalies.

1 files changed, 30 insertions, 0 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 893605499c..b605a44c87 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -51,6 +51,20 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
+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
@@ -841,6 +855,22 @@ 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