Merge branch 'experimental/master'

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