Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)

1 files changed, 12 insertions, 0 deletions

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