diff options
Diffstat (limited to 'toplevel/metasyntax.mli')
| -rw-r--r-- | toplevel/metasyntax.mli | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 34fbbef84..1eeec61b0 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -8,15 +8,21 @@ (*i $Id$ i*) +(*i*) +open Extend +open Vernacexpr +(*i*) + (* Adding grammar and pretty-printing objects in the environment *) -val add_syntax_obj : string -> Coqast.t list -> unit +val add_syntax_obj : string -> syntax_entry_ast list -> unit -val add_grammar_obj : string -> Coqast.t list -> unit +val add_grammar_obj : string -> grammar_entry_ast list -> unit val add_token_obj : string -> unit +val add_tactic_grammar : (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list -> unit val add_infix : - Gramext.g_assoc option -> int -> string -> Coqast.t -> unit + Gramext.g_assoc option -> int -> string -> Nametab.qualid Util.located -> unit val add_distfix : Gramext.g_assoc option -> int -> string -> Coqast.t -> unit |