diff options
Diffstat (limited to 'parsing/egramcoq.mli')
| -rw-r--r-- | parsing/egramcoq.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 9ae49f718a..19e8ee8f60 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -41,10 +41,8 @@ type notation_grammar = { } type tactic_grammar = { - tacgram_key : string; tacgram_level : int; tacgram_prods : grammar_prod_item list; - tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr; } (** {5 Adding notations} *) @@ -52,7 +50,7 @@ type tactic_grammar = { val extend_constr_grammar : Notation.level -> notation_grammar -> unit (** Add a term notation rule to the parsing system. *) -val extend_tactic_grammar : tactic_grammar -> unit +val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit (** Add a tactic notation rule to the parsing system. *) val recover_constr_grammar : notation -> Notation.level -> notation_grammar |