From d17a2e06c3ed54a7337d450cc197820638668e31 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 26 Apr 2016 15:51:38 +0200 Subject: [PATCH] Remove unused [iContradiction] tactic. --- proofmode/tactics.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/proofmode/tactics.v b/proofmode/tactics.v index 15d7aa249..30ddc4b77 100644 --- a/proofmode/tactics.v +++ b/proofmode/tactics.v @@ -97,8 +97,6 @@ Tactic Notation "iAssumption" := (** * False *) Tactic Notation "iExFalso" := apply tac_ex_falso. -Tactic Notation "iContradiction" constr(H) := iExFalso; iExact H. -Tactic Notation "iContradiction" := iExFalso; iAssumption. (** * Pure introduction *) Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := @@ -551,7 +549,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) := | IFrame => iFrame Hz | IName ?y => iRename Hz into y | IPersistent ?pat => iPersistent Hz; go Hz pat - | IList [[]] => iContradiction Hz + | IList [[]] => iExFalso; iExact Hz | IList [[?pat1; ?pat2]] => let Hy := iFresh in iSepDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2 | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2] -- GitLab