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 ++--------- vernac/metasyntax.mli | 4 ---- 2 files changed, 2 insertions(+), 13 deletions(-) (limited to 'vernac') 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 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