diff options
| -rw-r--r-- | ide/ide_slave.ml | 3 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 22 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 32 |
5 files changed, 4 insertions, 55 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bc7ce3883..65eececf7 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -466,9 +466,6 @@ let loop () = let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc)); - (* We'll handle goal fetching and display in our own way *) - Vernacentries.enable_goal_printing := false; - Vernacentries.qed_display_script := false; while not !quit do try let xml_query = Xml_parser.parse xml_ic in diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 17d8f5f49..9478542c1 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -345,7 +345,6 @@ let loop_flush_all () = let rec loop () = Sys.catch_break true; - if !Flags.print_emacs then Vernacentries.qed_display_script := false; try reset_input_buffer stdin top_buffer; (* Be careful to keep this loop tail-recursive *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c8f3ca1ab..6f9ffe02b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -250,7 +250,6 @@ let set_emacs () = if not (Option.is_empty !toploop) then error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; - Vernacentries.qed_display_script := false; color := `OFF (** Options for CoqIDE *) 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 |