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.mli | |
| 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.mli')
| -rw-r--r-- | vernac/pvernac.mli | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 2993a1661..b2f8f7146 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -16,21 +16,21 @@ val uvernac : gram_universe module Vernac_ : sig - val gallina : vernac_expr Gram.entry - val gallina_ext : vernac_expr Gram.entry - val command : vernac_expr Gram.entry - val syntax : vernac_expr Gram.entry - val vernac_control : vernac_control Gram.entry - val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val noedit_mode : vernac_expr Gram.entry - val command_entry : vernac_expr Gram.entry - val red_expr : raw_red_expr Gram.entry - val hint_info : Hints.hint_info_expr Gram.entry + val gallina : vernac_expr Entry.t + val gallina_ext : vernac_expr Entry.t + val command : vernac_expr Entry.t + val syntax : vernac_expr Entry.t + val vernac_control : vernac_control Entry.t + val rec_definition : (fixpoint_expr * decl_notation list) Entry.t + val noedit_mode : vernac_expr Entry.t + val command_entry : vernac_expr Entry.t + val red_expr : raw_red_expr Entry.t + val hint_info : Hints.hint_info_expr Entry.t end (** The main entry: reads an optional vernac command *) -val main_entry : (Loc.t * vernac_control) option Gram.entry +val main_entry : (Loc.t * vernac_control) option Entry.t (** Handling of the proof mode entry *) -val get_command_entry : unit -> vernac_expr Gram.entry -val set_command_entry : vernac_expr Gram.entry -> unit +val get_command_entry : unit -> vernac_expr Entry.t +val set_command_entry : vernac_expr Entry.t -> unit |