From 46856a80958f1aaa3242b6d37f018df9528e5e5f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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.ml  | 22 +++-------------------
 vernac/vernacentries.mli | 32 +-------------------------------
 2 files changed, 4 insertions(+), 50 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ca03ba3f3..5e5df9970 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -84,24 +84,10 @@ let show_universes () =
     Feedback.msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
     Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
 
-let show_prooftree () =
-  (* Spiwack: proof tree is currently not working *)
-  ()
-
-let enable_goal_printing = ref true
-
-let print_subgoals () =
-  if !enable_goal_printing && is_verbose ()
-  then begin
-    Feedback.msg_notice (pr_open_subgoals ())
-  end
-
-let try_print_subgoals () =
-  try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ()
-
-
-  (* Simulate the Intro(s) tactic *)
+(* Spiwack: proof tree is currently not working *)
+let show_prooftree () = ()
 
+(* Simulate the Intro(s) tactic *)
 let show_intro all =
   let pf = get_pftreestate() in
   let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
@@ -511,8 +497,6 @@ let vernac_start_proof locality p kind l lettop =
 	(str "Let declarations can only be used in proof editing mode.");
   start_proof_and_print (local, p, Proof kind) l no_hook
 
-let qed_display_script = ref true
-
 let vernac_end_proof ?proof = function
   | Admitted          -> save_proof ?proof Admitted
   | Proved (_,_) as e -> save_proof ?proof e
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