Merge PR#765: Remove obsolete Show commands

7 files changed, 0 insertions, 63 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 0760d716e..b66659dc8 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -427,22 +427,6 @@ This command displays the current goals.
   This tactics script may contain some holes (subgoals not yet proved).
   They are printed under the form \verb!<Your Tactic Text here>!.
 
-%% \item {\tt Show Tree.}\comindex{Show Tree}\\
-%% This command can be seen as a more structured way of
-%% displaying the state of the proof than that 
-%% provided by {\tt Show Script}. Instead of just giving
-%% the list of tactics that have been applied, it 
-%% shows the derivation tree constructed by then. 
-%% Each node of the tree contains the conclusion
-%% of the corresponding sub-derivation (i.e. a
-%% goal with its corresponding local context) and 
-%% the tactic that has generated all the 
-%% sub-derivations. The leaves of this tree are
-%% the goals which still remain to be proved.
-
-%\item {\tt Show Node}\comindex{Show Node}\\
-%        Not yet documented
-
 \item {\tt Show Proof.}\comindex{Show Proof}\\
 It displays the proof term generated by the 
 tactics that have been applied. 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f405100b1..f0ee1d58a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -181,9 +181,6 @@ let print_projections = ref false
 
 let print_meta_as_hole = ref false
 
-let with_arguments f = Flags.with_option print_arguments f
-let with_implicits f = Flags.with_option print_implicits f
-let with_coercions f = Flags.with_option print_coercions f
 let with_universes f = Flags.with_option print_universes f
 let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
 let without_symbols f = Flags.with_option print_no_symbol f
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index d771ee86f..6c82168e4 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -59,16 +59,6 @@ val set_extern_reference :
 val get_extern_reference :
   unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
 
-(** This governs printing of implicit arguments. If [with_implicits] is
-   on and not [with_arguments] then implicit args are printed prefixed
-   by "!"; if [with_implicits] and [with_arguments] are both on the
-   function and not the arguments is prefixed by "!" *)
-val with_implicits : ('a -> 'b) -> 'a -> 'b
-val with_arguments : ('a -> 'b) -> 'a -> 'b
-
-(** This forces printing of coercions *)
-val with_coercions : ('a -> 'b) -> 'a -> 'b
-
 (** This forces printing universe names of Type\{.\} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b
 
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index ab440c6b7..cabd06735 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -96,17 +96,13 @@ type locatable =
 
 type showable =
   | ShowGoal of goal_reference
-  | ShowGoalImplicitly of int option
   | ShowProof
-  | ShowNode
   | ShowScript
   | ShowExistentials
   | ShowUniverses
-  | ShowTree
   | ShowProofNames
   | ShowIntros of bool
   | ShowMatch of reference
-  | ShowThesis
 
 type comment =
   | CommentConstr of constr_expr
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index a3f9793bb..e96a68bc6 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -64,22 +64,14 @@ GEXTEND Gram
       | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
       | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
       | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id))
-      | IDENT "Show"; IDENT "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal")))
-      | IDENT "Show"; IDENT "Goal"; n = string ->
-          VernacShow (ShowGoal (GoalUid n))
-      | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
-	  VernacShow (ShowGoalImplicitly n)
-      | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
       | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript
       | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials
       | IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses
-      | IDENT "Show"; IDENT "Tree" -> VernacShow ShowTree
       | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames
       | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
       | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
       | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
       | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id)
-      | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis
       | IDENT "Guarded" -> VernacCheckGuard
       (* Hints for Auto and EAuto *)
       | IDENT "Create"; IDENT "HintDb" ;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 781af4789..9d28bc4f8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -561,17 +561,13 @@ open Decl_kinds
           | GoalUid n -> spc () ++ str n in
         let pr_showable = function
           | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
-          | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n
           | ShowProof -> keyword "Show Proof"
-          | ShowNode -> keyword "Show Node"
           | ShowScript -> keyword "Show Script"
           | ShowExistentials -> keyword "Show Existentials"
           | ShowUniverses -> keyword "Show Universes"
-          | ShowTree -> keyword "Show Tree"
           | ShowProofNames -> keyword "Show Conjectures"
           | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
           | ShowMatch id -> keyword "Show Match " ++ pr_reference id
-          | ShowThesis -> keyword "Show Thesis"
         in
         return (pr_showable s)
       | VernacCheckGuard ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b7..6830a5da1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -61,13 +61,6 @@ let show_proof () =
   let pprf = Proof.partial_proof p in
   Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf)
 
-let show_node () =
-  (* spiwack: I'm have little clue what this function used to do. I deactivated it, 
-      could, possibly, be cleaned away. (Feb. 2010) *)
-  ()
-
-let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.")
-
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
   let pfts = get_pftreestate () in
@@ -83,9 +76,6 @@ let show_universes () =
     Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
     Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
 
-(* Spiwack: proof tree is currently not working *)
-let show_prooftree () = ()
-
 (* Simulate the Intro(s) tactic *)
 let show_intro all =
   let open EConstr in
@@ -1844,21 +1834,13 @@ let vernac_show = let open Feedback in function
       | GoalUid id -> pr_goal_by_uid id
     in
     msg_notice info
-  | ShowGoalImplicitly None ->
-      Constrextern.with_implicits msg_notice (pr_open_subgoals ())
-  | ShowGoalImplicitly (Some n) ->
-      Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n)
   | ShowProof -> show_proof ()
-  | ShowNode -> show_node ()
   | ShowExistentials -> show_top_evars ()
   | ShowUniverses -> show_universes ()
-  | ShowTree -> show_prooftree ()
   | ShowProofNames ->
       msg_notice (pr_sequence pr_id (Pfedit.get_all_proof_names()))
   | ShowIntros all -> show_intro all
   | ShowMatch id -> show_match id
-  | ShowThesis -> show_thesis ()
-
 
 let vernac_check_guard () =
   let pts = get_pftreestate () in