diff options
| author | Pierre-Marie Pédrot | 2016-03-19 01:34:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-19 01:35:14 +0100 |
| commit | f63cf9d72c7feb6aa65e525bf6262559a355435f (patch) | |
| tree | 82264308c979e846501e86634f319f7caf10a048 /parsing/egramml.mli | |
| parent | 13c50b98b0a294a6056d2e00a0de44cedca7af12 (diff) | |
| parent | 25f39e54e4e8eaf08865121f06635dc3bd1092da (diff) | |
Cleaning up and extending the expressivity of Pcoq.
Diffstat (limited to 'parsing/egramml.mli')
| -rw-r--r-- | parsing/egramml.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/egramml.mli b/parsing/egramml.mli index edf971574d..1ad9472007 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -16,7 +16,7 @@ open Vernacexpr type 's grammar_prod_item = | GramTerminal of string | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type * - ('s, 'a) Pcoq.entry_key -> 's grammar_prod_item + ('s, 'a) Extend.symbol -> 's grammar_prod_item val extend_vernac_command_grammar : Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option -> |