diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
commit | f219abfed720305c13875c3c63f9240cf63f78bc (patch) | |
tree | 69d2c026916128fdb50b8d1c0dbf1be451340d30 /toplevel/metasyntax.mli | |
parent | 476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff) | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Merge tag 'upstream/8.5_beta1+dfsg'
Upstream version 8.5~beta1+dfsg
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 |