diff options
| author | glondu | 2010-10-06 18:57:04 +0000 |
|---|---|---|
| committer | glondu | 2010-10-06 18:57:04 +0000 |
| commit | 2fe6aa3b4d422ec092844e84c4d15f5c1414b442 (patch) | |
| tree | 55b5e6255d514cc05b72b0041fd567dd0d11132d /parsing | |
| parent | b36e75cca2ea910dead09864c4f10ba79b894a35 (diff) | |
Remove Explain* vernacs
Basically untouched since 1999. Same fate as VernacGo (r13506).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 4 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 2 |
2 files changed, 0 insertions, 6 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index b5bac26c3f..e23ef91439 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -80,10 +80,6 @@ GEXTEND Gram | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis - | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer -> - VernacShow (ExplainProof l) - | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> - VernacShow (ExplainTree l) | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 24c9d9d8ac..0a65578f17 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -464,8 +464,6 @@ let rec pr_vernac = function | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro") | ShowMatch id -> str"Show Match " ++ pr_lident id | ShowThesis -> str "Show Thesis" - | ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l - | ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l in pr_showable s | VernacCheckGuard -> str"Guarded" |