diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-12 11:25:26 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-12 11:25:26 +0200 |
| commit | 3813ba5229cf42597cd30a08e842e0832e5253cb (patch) | |
| tree | 0b63fd48d2b021bba3e7518652ac4bc2c5ccc8e4 | |
| parent | 6cd14bf253f681d0465f8dce1d84a54a4f104d9c (diff) | |
Remove Show Thesis command which was never implemented.
| -rw-r--r-- | intf/vernacexpr.ml | 1 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 1 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
4 files changed, 0 insertions, 7 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index b3b332727..cabd06735 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -103,7 +103,6 @@ type showable = | 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 b5eb2a181..e96a68bc6 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -72,7 +72,6 @@ GEXTEND Gram | 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 81f41cba1..9d28bc4f8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -568,7 +568,6 @@ open Decl_kinds | 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 e0eeaf563..6830a5da1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -61,8 +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_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 @@ -1843,8 +1841,6 @@ let vernac_show = let open Feedback in function 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 |