From ef29c0a927728d9cf4a45bc3c26d2393d753184e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 12:24:58 +0200 Subject: Introduce a Pcoq.Entry module for functions that ought to be exported. We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins. --- vernac/g_vernac.mlg | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'vernac/g_vernac.mlg') diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3a01ce6df..2c60abfe3 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -37,18 +37,18 @@ let _ = List.iter CLexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) -let query_command = Gram.entry_create "vernac:query_command" - -let subprf = Gram.entry_create "vernac:subprf" - -let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" -let thm_token = Gram.entry_create "vernac:thm_token" -let def_body = Gram.entry_create "vernac:def_body" -let decl_notation = Gram.entry_create "vernac:decl_notation" -let record_field = Gram.entry_create "vernac:record_field" -let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" -let instance_name = Gram.entry_create "vernac:instance_name" -let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" +let query_command = Entry.create "vernac:query_command" + +let subprf = Entry.create "vernac:subprf" + +let class_rawexpr = Entry.create "vernac:class_rawexpr" +let thm_token = Entry.create "vernac:thm_token" +let def_body = Entry.create "vernac:def_body" +let decl_notation = Entry.create "vernac:decl_notation" +let record_field = Entry.create "vernac:record_field" +let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" +let instance_name = Entry.create "vernac:instance_name" +let section_subset_expr = Entry.create "vernac:section_subset_expr" let make_bullet s = let open Proof_bullet in -- cgit v1.2.3