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/egramml.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/egramml.mli') diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 31aa1a989..a5ee036db 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -21,7 +21,7 @@ type 's grammar_prod_item = ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : - Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option -> + Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option -> vernac_expr grammar_prod_item list -> unit val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list -- cgit v1.2.3