diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-22 02:08:29 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-12 16:49:46 +0200 |
| commit | 46856a80958f1aaa3242b6d37f018df9528e5e5f (patch) | |
| tree | 3c15b53a6f6ff36629e7fbff317ee73cc9ed818f /vernac/vernacentries.mli | |
| parent | ce2b2058587224ade9261cd4127ef4f6e94d356b (diff) | |
[vernac] vernacentries.mli cleanup
This header file had accumulated quite a bit of cruft over the
years, we clean it up while we are at it.
No functional change as all the removed variables/methods were noops
long time ago.
Diffstat (limited to 'vernac/vernacentries.mli')
| -rw-r--r-- | vernac/vernacentries.mli | 32 |
1 files changed, 1 insertions, 31 deletions
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 7cdc8dd06..fb2899515 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -11,42 +11,15 @@ open Misctypes val dump_global : Libnames.reference or_by_notation -> unit (** Vernacular entries *) - -val show_prooftree : unit -> unit - -val show_node : unit -> unit - val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit -(** This function can be used by any command that want to observe terms - in the context of the current goal *) -val get_current_context_of_args : int option -> Evd.evar_map * Environ.env - (** The main interpretation function of vernacular expressions *) -val interp : +val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> Loc.t * Vernacexpr.vernac_expr -> unit -(** Print subgoals when the verbose flag is on. - Meant to be used inside vernac commands from plugins. *) - -val print_subgoals : unit -> unit -val try_print_subgoals : unit -> unit - -(** The printing of goals via [print_subgoals] or during - [interp] can be controlled by the following flag. - Used for instance by coqide, since it has its own - goal-fetching mechanism. *) - -val enable_goal_printing : bool ref - -(** Should Qed try to display the proof script ? - True by default, but false in ProofGeneral and coqIDE *) - -val qed_display_script : bool ref - (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name followed by enough pattern variables. @@ -55,9 +28,6 @@ val qed_display_script : bool ref val make_cases : string -> string list list -val vernac_end_proof : - ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit - val with_fail : bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind |