diff options
Diffstat (limited to 'parsing/egramcoq.mli')
| -rw-r--r-- | parsing/egramcoq.mli | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 6ec106626..1fe06a29d 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -36,20 +36,6 @@ type notation_grammar = { notgram_typs : notation_var_internalization_type list; } -(** {5 Extending the parser with Summary-synchronized commands} *) - -type 'a grammar_command -(** Type of synchronized parsing extensions. The ['a] type should be - marshallable. *) - -val create_grammar_command : string -> ('a -> int) -> 'a grammar_command -(** Create a new grammar-modifying command with the given name. The function - should modify the parser state and return the number of grammar extensions - performed. *) - -val extend_grammar : 'a grammar_command -> 'a -> unit -(** Extend the grammar of Coq with the given data. *) - (** {5 Adding notations} *) val extend_constr_grammar : Notation.level -> notation_grammar -> unit @@ -58,5 +44,3 @@ val extend_constr_grammar : Notation.level -> notation_grammar -> unit 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 |