diff options
Diffstat (limited to 'toplevel/metasyntax.mli')
| -rw-r--r-- | toplevel/metasyntax.mli | 25 |
1 files changed, 15 insertions, 10 deletions
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index f3bdf833..38a37757 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -1,27 +1,30 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names -open Libnames -open Ppextend -open Extend open Tacexpr open Vernacexpr open Notation -open Topconstr +open Constrexpr +open Notation_term val add_token_obj : string -> unit (** Adding a tactic notation in the environment *) val add_tactic_notation : - int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit + locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> + unit + +type atomic_entry = string * Genarg.glob_generic_argument list option + +val add_ml_tactic_notation : ml_tactic_name -> + Egramml.grammar_prod_item list list -> atomic_entry list -> unit (** Adding a (constr) notation in the environment*) @@ -31,10 +34,12 @@ val add_infix : locality_flag -> (lstring * syntax_modifier list) -> val add_notation : locality_flag -> constr_expr -> (lstring * syntax_modifier list) -> scope_name option -> unit +val add_notation_extra_printing_rule : string -> string -> string -> unit + (** Declaring delimiter keys and default scopes *) val add_delimiters : scope_name -> string -> unit -val add_class_scope : scope_name -> Classops.cl_typ -> unit +val add_class_scope : scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) @@ -53,12 +58,12 @@ val add_syntax_extension : (** Add a syntactic definition (as in "Notation f := ...") *) -val add_syntactic_definition : identifier -> identifier list * constr_expr -> +val add_syntactic_definition : Id.t -> Id.t list * constr_expr -> bool -> Flags.compat_version option -> unit (** Print the Camlp4 state of a grammar *) -val print_grammar : string -> unit +val pr_grammar : string -> Pp.std_ppcmds val check_infix_modifiers : syntax_modifier list -> unit |