diff options
Diffstat (limited to 'parsing/egramcoq.mli')
| -rw-r--r-- | parsing/egramcoq.mli | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 153f7528ff..6ec1066260 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -36,11 +36,6 @@ type notation_grammar = { notgram_typs : notation_var_internalization_type list; } -type tactic_grammar = { - tacgram_level : int; - tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list; -} - (** {5 Extending the parser with Summary-synchronized commands} *) type 'a grammar_command @@ -60,24 +55,8 @@ val extend_grammar : 'a grammar_command -> 'a -> unit val extend_constr_grammar : Notation.level -> notation_grammar -> unit (** Add a term notation rule to the parsing system. *) -val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit -(** Add a tactic notation rule to the parsing system. This produces a TacAlias - tactic with the provided kernel name. *) - -val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> Tacexpr.raw_tactic_expr grammar_prod_item list list -> unit -(** Add a ML tactic notation rule to the parsing system. This produces a - TacML tactic with the provided string as name. *) - val recover_constr_grammar : notation -> Notation.level -> notation_grammar (** For a declared grammar, returns the rule + the ordered entry types of variables in the rule (for use in the interpretation) *) val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b - -(** {5 Adding tactic quotations} *) - -val create_ltac_quotation : string -> - ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Gram.entry * int option) -> unit -(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is, - Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and - generates an argument using [f] on the entry parsed by [e]. *) |