Moving the grammar summary to Pcoq.

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