From 46856a80958f1aaa3242b6d37f018df9528e5e5f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Feb 2017 02:08:29 +0100 Subject: [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. --- vernac/vernacentries.mli | 32 +------------------------------- 1 file changed, 1 insertion(+), 31 deletions(-) (limited to 'vernac/vernacentries.mli') 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 -- cgit v1.2.3