diff options
| author | Pierre-Marie Pédrot | 2016-03-17 16:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-17 21:08:26 +0100 |
| commit | 4b2cdf733df6dc23247b078679e71da98e54f5cc (patch) | |
| tree | ac05560456999b14a897e1701ae6678ab5c6e6b7 /plugins/setoid_ring | |
| parent | 4d13842869647790c9bd3084dce672fee7b648a1 (diff) | |
Removing the special status of generic entries defined by Coq itself.
The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.
After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 856ec0db5f..cd1d704dde 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -14,6 +14,11 @@ open Libnames open Printer open Newring_ast open Newring +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "newring_plugin" |