diff options
Diffstat (limited to 'parsing/egrammar.mli')
| -rw-r--r-- | parsing/egrammar.mli | 50 |
1 files changed, 29 insertions, 21 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index ade91453..31247044 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -6,54 +6,62 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: egrammar.mli,v 1.14.2.6 2005/12/23 22:16:46 herbelin Exp $ i*) +(*i $Id: egrammar.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) (*i*) open Util open Topconstr -open Ast -open Coqast +open Pcoq +open Extend open Vernacexpr open Ppextend -open Extend open Rawterm +open Mod_subst (*i*) +(** Mapping of grammar productions to camlp4 actions + Used for Coq-level Notation and Tactic Notation, + and for ML-level tactic and vernac extensions + *) + +type prod_item = + | Term of Token.pattern + | NonTerm of constr_production_entry * + (Names.identifier * constr_production_entry) option + type notation_grammar = - int * Gramext.g_assoc option * notation * prod_item list * int list option + int * Gramext.g_assoc option * notation * prod_item list type all_grammar_command = | Notation of (precedence * tolerability list) * notation_grammar - | Grammar of grammar_command | TacticGrammar of - (string * (string * grammar_production list) * - (Names.dir_path * Tacexpr.raw_tactic_expr)) - list * (string * Genarg.argument_type list * - (string * Pptactic.grammar_terminals)) list + (string * int * grammar_production list * + (Names.dir_path * Tacexpr.glob_tactic_expr)) val extend_grammar : all_grammar_command -> unit (* Add grammar rules for tactics *) + type grammar_tactic_production = | TacTerm of string - | TacNonTerm of loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option + | TacNonTerm of + loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option val extend_tactic_grammar : - string -> (string * grammar_tactic_production list) list -> unit + string -> grammar_tactic_production list list -> unit val extend_vernac_command_grammar : - string -> (string * grammar_tactic_production list) list -> unit - + string -> grammar_tactic_production list list -> unit +(* val get_extend_tactic_grammars : - unit -> (string * (string * grammar_tactic_production list) list) list + unit -> (string * grammar_tactic_production list list) list +*) val get_extend_vernac_grammars : - unit -> (string * (string * grammar_tactic_production list) list) list + unit -> (string * grammar_tactic_production list list) list +(* val reset_extend_grammars_v8 : unit -> unit - -val subst_all_grammar_command : - Names.substitution -> all_grammar_command -> all_grammar_command - -val interp_entry_name : string -> string -> +*) +val interp_entry_name : int -> string -> string -> entry_type * Token.t Gramext.g_symbol val recover_notation_grammar : |