diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-22 12:24:58 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-07 16:34:44 +0200 |
commit | ef29c0a927728d9cf4a45bc3c26d2393d753184e (patch) | |
tree | d43b108a24ac69f7fbcdd184781141fea36a1dd5 /toplevel/g_toplevel.mlg | |
parent | 4b3187a635864f8faa2d512775231a4e6d204c51 (diff) |
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.
Diffstat (limited to 'toplevel/g_toplevel.mlg')
-rw-r--r-- | toplevel/g_toplevel.mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 53d3eef23..5aba3d6b0 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -21,9 +21,9 @@ type vernac_toplevel = | VernacControl of vernac_control module Toplevel_ : sig - val vernac_toplevel : vernac_toplevel CAst.t Gram.entry + val vernac_toplevel : vernac_toplevel CAst.t Entry.t end = struct - let gec_vernac s = Gram.entry_create ("toplevel:" ^ s) + let gec_vernac s = Entry.create ("toplevel:" ^ s) let vernac_toplevel = gec_vernac "vernac_toplevel" end @@ -49,6 +49,6 @@ END { -let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa +let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa } |