diff options
Diffstat (limited to 'parsing/egrammar.mli')
| -rw-r--r-- | parsing/egrammar.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 73f9e424e..ff3f6284b 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -9,11 +9,12 @@ (*i $Id$ i*) (*i*) -open Coqast +open Topconstr open Ast open Coqast open Vernacexpr open Extend +open Rawterm (*i*) type frozen_t @@ -23,11 +24,15 @@ val unfreeze : frozen_t -> unit val init : unit -> unit type all_grammar_command = - | AstGrammar of grammar_command + | Notation of (string * notation * prod_item list) + | Delimiters of (scope_name * prod_item list * prod_item list) + | Grammar of grammar_command | TacticGrammar of (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list val extend_grammar : all_grammar_command -> unit +val extend_constr_grammar : string * aconstr * prod_item list -> unit + (* Add grammar rules for tactics *) type grammar_tactic_production = | TacTerm of string |