diff options
| author | Pierre-Marie Pédrot | 2014-09-09 22:13:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-10 00:16:20 +0200 |
| commit | edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 (patch) | |
| tree | e7af11e344a99b2496d22d2bc100f493bd701b96 /parsing/egramml.mli | |
| parent | 0dd3f0d34873dcd126be8ec48724a310214f38ac (diff) | |
VernacExtend does not dispatch on type anymore.
Diffstat (limited to 'parsing/egramml.mli')
| -rw-r--r-- | parsing/egramml.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 9e2c29b98a..97bfbf682d 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -17,11 +17,10 @@ type grammar_prod_item = Pcoq.prod_entry_key * Names.Id.t option val extend_vernac_command_grammar : - string -> Vernacexpr.vernac_expr Pcoq.Gram.entry option -> - grammar_prod_item list list -> unit + Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option -> + grammar_prod_item list -> unit -val get_extend_vernac_grammars : - unit -> (string * grammar_prod_item list list) list +val get_extend_vernac_rule : Vernacexpr.extend_name -> grammar_prod_item list (** Utility function reused in Egramcoq : *) |