diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 8 | ||||
| -rw-r--r-- | parsing/egramcoq.mli | 24 |
2 files changed, 17 insertions, 15 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 2e83c2b6b9..fcb4e7d7e1 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -290,7 +290,13 @@ let extend_grammar gram = | TacticGrammar g -> add_tactic_entry g in grammar_state := (nb,gram) :: !grammar_state -let recover_notation_grammar ntn prec = +let extend_constr_grammar pr typs ntn = + extend_grammar (Notation (pr, typs, ntn)) + +let extend_tactic_grammar ntn = + extend_grammar (TacticGrammar ntn) + +let recover_constr_grammar ntn prec = let filter = function | _, Notation (prec', vars, ng) when Notation.level_eq prec prec' && diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 7cf3bab69a..dfae42ae4c 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -46,28 +46,24 @@ type tactic_grammar = { tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr; } -(** Adding notations *) +(** {5 Adding notations} *) -type all_grammar_command = - | Notation of - (precedence * tolerability list) - * notation_var_internalization_type list - (** not needed for defining grammar, hosted by egrammar for - transmission to interp_aconstr (via recover_notation_grammar) *) - * notation_grammar - | TacticGrammar of tactic_grammar +val extend_constr_grammar : + Notation.level -> notation_var_internalization_type list -> + notation_grammar -> unit +(** Add a term notation rule to the parsing system. *) -val extend_grammar : all_grammar_command -> unit +val extend_tactic_grammar : tactic_grammar -> unit +(** Add a tactic notation rule to the parsing system. *) +val recover_constr_grammar : notation -> Notation.level -> + notation_var_internalization_type list * notation_grammar (** For a declared grammar, returns the rule + the ordered entry types of variables in the rule (for use in the interpretation) *) -val recover_notation_grammar : - notation -> (precedence * tolerability list) -> - notation_var_internalization_type list * notation_grammar val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b -(** Adding tactic quotations *) +(** {5 Adding tactic quotations} *) val create_ltac_quotation : string -> ('grm Loc.located -> 'raw) -> ('raw, 'glb, 'top) genarg_type -> 'grm Gram.entry -> unit |