From 69822345c198aa6bf51354f6b84c7fd5d401bc9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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.
---
 parsing/pcoq.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 54e7949aea..ddb26d7717 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -638,3 +638,15 @@ let () =
   Grammar.register0 wit_constr (Constr.constr);
   Grammar.register0 wit_red_expr (Vernac_.red_expr);
   ()
+
+(** Registering extra grammar *)
+
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
+
+let register_grammars_by_name name grams =
+  grammar_names := String.Map.add name grams !grammar_names
+
+let find_grammars_by_name name =
+  String.Map.find name !grammar_names
-- 
cgit v1.2.3