Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 25 insertions, 30 deletions

diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index be90cd7a..71522567 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: metasyntax.mli,v 1.26.2.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: metasyntax.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -15,49 +15,44 @@ open Ppextend
 open Extend
 open Tacexpr
 open Vernacexpr
-open Symbols
+open Notation
 open Topconstr
 (*i*)
 
-(* Adding grammar and pretty-printing objects in the environment *)
+val add_token_obj : string -> unit
 
-val add_syntax_obj : string -> raw_syntax_entry list -> unit
+(* Adding a tactic notation in the environment *)
 
-val add_grammar_obj : string -> raw_grammar_entry list -> unit
-val add_token_obj : string -> unit
-val add_tactic_grammar :
-  (string * (string * grammar_production list) * raw_tactic_expr) list -> unit
+val add_tactic_notation : 
+  int * grammar_production list * raw_tactic_expr -> unit
+
+(* Adding a (constr) notation in the environment*)
 
 val add_infix : locality_flag -> (string * syntax_modifier list) ->
-  reference -> (string * syntax_modifier list) option ->
-    scope_name option -> unit
-val add_distfix : locality_flag ->
-  grammar_associativity -> precedence -> string -> reference
-    -> scope_name option -> unit
-val translate_distfix : grammar_associativity -> string -> reference ->
-  Gramext.g_assoc * string * constr_expr
+  reference -> scope_name option -> unit
+
+val add_notation : locality_flag -> constr_expr ->
+  (string * syntax_modifier list) -> scope_name option -> 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_notation : locality_flag -> constr_expr
-  -> (string * syntax_modifier list) option
-  -> (string * syntax_modifier list) option
-      -> scope_name option -> unit
+(* Add only the interpretation of a notation that already has pa/pp rules *)
 
-val add_notation_interpretation : string -> Constrintern.implicits_env
-  -> constr_expr -> scope_name option -> unit
+val add_notation_interpretation : string -> Constrintern.implicits_env ->
+  constr_expr -> scope_name option -> unit
 
-val add_syntax_extension : locality_flag
-  -> (string * syntax_modifier list) option
-  -> (string * syntax_modifier list) option -> unit
+(* Add only the parsing/printing rule of a notation *)
 
-val print_grammar : string -> string -> unit
+val add_syntax_extension : 
+  locality_flag -> (string * syntax_modifier list) -> unit
 
-val merge_modifiers : Gramext.g_assoc option -> int option -> 
-  syntax_modifier list -> syntax_modifier list
+(* Print the Camlp4 state of a grammar *)
+
+val print_grammar : string -> string -> unit
 
-val interp_infix_modifiers : syntax_modifier list ->
-  Gramext.g_assoc option * precedence option * bool * string located option
+(* Removes quotes in a notation *)
 
-val standardise_locatable_notation : string -> string
+val standardize_locatable_notation : string -> string