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 /vernac/pvernac.ml | |
| 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 'vernac/pvernac.ml')
| -rw-r--r-- | vernac/pvernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index aea66a07a..b2fa8ec99 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -14,7 +14,7 @@ let uvernac = create_universe "vernac" module Vernac_ = struct - let gec_vernac s = Gram.entry_create ("vernac:" ^ s) + let gec_vernac s = Entry.create ("vernac:" ^ s) (* The different kinds of vernacular commands *) let gallina = gec_vernac "gallina" @@ -26,7 +26,7 @@ module Vernac_ = let red_expr = new_entry utactic "red_expr" let hint_info = gec_vernac "hint_info" (* Main vernac entry *) - let main_entry = Gram.entry_create "vernac" + let main_entry = Entry.create "vernac" let noedit_mode = gec_vernac "noedit_command" let () = |