From 69822345c198aa6bf51354f6b84c7fd5d401bc9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 Aug 2017 20:32:15 +0200
Subject: Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.

Renaming it register_grammars_by_name.
---
 vernac/metasyntax.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'vernac/metasyntax.mli')

diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index e064b570e..9137f7a7e 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -55,10 +55,6 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
 
 val pr_grammar : string -> Pp.t
 
-type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
-
-val register_grammar : string -> any_entry list -> unit
-
 val check_infix_modifiers : syntax_modifier list -> unit
 
 val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
-- 
cgit v1.2.3