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 /grammar | |
| 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 'grammar')
| -rw-r--r-- | grammar/q_util.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 34f1cf6cb6..6e491b076f 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -60,5 +60,5 @@ let rec mlexpr_of_prod_entry_key = function | Pcoq.Anext -> <:expr< Pcoq.Anext >> | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >> | Pcoq.Agram s -> Errors.anomaly (Pp.str "Agram not supported") - | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >> + | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.name $lid:s$) >> | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> |