diff options
author | 2016-06-23 15:11:16 +0200 | |
---|---|---|
committer | 2017-06-14 12:02:35 +0200 | |
commit | a4faac6d24d28ae49ff38477f92f85aef6759075 (patch) | |
tree | 451c74db0dba5c0c87c2a92bdea953910ad49f27 /plugins/funind/Recdef.v | |
parent | 706b16c3c714f91bfff33ce340aec6f2d24fe246 (diff) |
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.
Diffstat (limited to 'plugins/funind/Recdef.v')
0 files changed, 0 insertions, 0 deletions