diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 02:35:56 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:00 -0400 |
| commit | 13929f39f8560cfcb3aacf20c84c6dcb5295cec5 (patch) | |
| tree | a4204cd4bced576d6d846ebac908aab5092c66a5 /vernac/vernacextend.mli | |
| parent | 4a88beff476d2c27eae381bc8a61f777015c0617 (diff) | |
[parsing] Make grammar extension type private.
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
Diffstat (limited to 'vernac/vernacextend.mli')
| -rw-r--r-- | vernac/vernacextend.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 90c00415d4..0acb5f43f9 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -111,7 +111,7 @@ type 'a argument_rule = | Arg_alias of 'a Pcoq.Entry.t (** This is used because CAMLP5 parser can be dumb about rule factorization, which sometimes requires two entries to be the same. *) -| Arg_rules of 'a Extend.production_rule list +| Arg_rules of 'a Pcoq.production_rule list (** There is a discrepancy here as we use directly extension rules and thus entries instead of ty_user_symbol and thus arguments as roots. *) |