aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-17 16:57:05 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-17 21:08:26 +0100
commit4b2cdf733df6dc23247b078679e71da98e54f5cc (patch)
treeac05560456999b14a897e1701ae6678ab5c6e6b7 /plugins/romega
parent4d13842869647790c9bd3084dce672fee7b648a1 (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/romega')
-rw-r--r--plugins/romega/g_romega.ml42
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 6b2b2bbfa..61efa9f54 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -12,6 +12,8 @@ DECLARE PLUGIN "romega_plugin"
open Names
open Refl_omega
+open Constrarg
+open Pcoq.Prim
let eval_tactic name =
let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in