diff options
Diffstat (limited to 'toplevel/metasyntax.mli')
| -rw-r--r-- | toplevel/metasyntax.mli | 26 |
1 files changed, 12 insertions, 14 deletions
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 2c4e29bb..38a0ae59 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: metasyntax.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Libnames @@ -18,16 +15,15 @@ open Tacexpr open Vernacexpr open Notation open Topconstr -(*i*) val add_token_obj : string -> unit -(* Adding a tactic notation in the environment *) +(** Adding a tactic notation in the environment *) val add_tactic_notation : int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit -(* Adding a (constr) notation in the environment*) +(** Adding a (constr) notation in the environment*) val add_infix : locality_flag -> (lstring * syntax_modifier list) -> constr_expr -> scope_name option -> unit @@ -35,33 +31,35 @@ val add_infix : locality_flag -> (lstring * syntax_modifier list) -> val add_notation : locality_flag -> constr_expr -> (lstring * syntax_modifier list) -> scope_name option -> unit -(* Declaring delimiter keys and default scopes *) +(** Declaring delimiter keys and default scopes *) val add_delimiters : scope_name -> string -> unit val add_class_scope : scope_name -> Classops.cl_typ -> unit -(* Add only the interpretation of a notation that already has pa/pp rules *) +(** Add only the interpretation of a notation that already has pa/pp rules *) val add_notation_interpretation : (lstring * constr_expr * scope_name option) -> unit -(* Add a notation interpretation for supporting the "where" clause *) +(** Add a notation interpretation for supporting the "where" clause *) val set_notation_for_interpretation : Constrintern.internalization_env -> (lstring * constr_expr * scope_name option) -> unit -(* Add only the parsing/printing rule of a notation *) +(** Add only the parsing/printing rule of a notation *) val add_syntax_extension : locality_flag -> (lstring * syntax_modifier list) -> unit -(* Add a syntactic definition (as in "Notation f := ...") *) +(** Add a syntactic definition (as in "Notation f := ...") *) val add_syntactic_definition : identifier -> identifier list * constr_expr -> - bool -> bool -> unit + bool -> Flags.compat_version option -> unit -(* Print the Camlp4 state of a grammar *) +(** Print the Camlp4 state of a grammar *) val print_grammar : string -> unit val check_infix_modifiers : syntax_modifier list -> unit + +val with_syntax_protection : ('a -> 'b) -> 'a -> 'b |