diff options
| author | Pierre-Marie Pédrot | 2014-02-16 04:17:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-02-16 14:36:15 +0100 |
| commit | abd83cffe1afe6745775c67b8c827038e295a1d2 (patch) | |
| tree | 047668419f552be8e803cd6e558bae917c5d49e6 /tactics | |
| parent | f4d6b4bce315639008b52727f741de82e2687d7e (diff) | |
Removing non-marshallable data from the Agram constructor. Instead of
containing opaque grammar objects, it now contains a string representing
the entry. In order to recover the entry from the string, the former must
have been created with [Pcoq.create_generic_entry] or similar. This is
guaranteed for entries generated by ARGUMENT EXTEND, and must be done by
hand otherwise.
Some plugins were fixed accordingly.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/g_rewrite.ml4 | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index db98c42503..03bbc4b046 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -25,7 +25,6 @@ open Tacmach open Tacticals open Tactics open Rewrite -open Pcoq.Constr type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings @@ -200,6 +199,16 @@ type binders_argtype = local_binder list let wit_binders = (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type) +let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders) + +open Pcoq + +GEXTEND Gram + GLOBAL: binders; + binders: + [ [ b = Pcoq.Constr.binders -> b ] ]; +END + VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) |