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. --- vernac/metasyntax.ml | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'vernac/metasyntax.ml') diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index a1c8902c5..da8dda9c2 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -43,13 +43,6 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s) let entry_buf = Buffer.create 64 -type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry - -let grammars : any_entry list String.Map.t ref = ref String.Map.empty - -let register_grammar name grams = - grammars := String.Map.add name grams !grammars - let pr_entry e = let () = Buffer.clear entry_buf in let ft = Format.formatter_of_buffer entry_buf in @@ -57,11 +50,11 @@ let pr_entry e = str (Buffer.contents entry_buf) let pr_registered_grammar name = - let gram = try Some (String.Map.find name !grammars) with Not_found -> None in + let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in match gram with | None -> user_err Pp.(str "Unknown or unprintable grammar entry.") | Some entries -> - let pr_one (AnyEntry e) = + let pr_one (Pcoq.AnyEntry e) = str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++ pr_entry e in -- cgit v1.2.3