Skip to content
Snippets Groups Projects
Commit d17a2e06 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove unused [iContradiction] tactic.

parent 10a93b0b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 3 deletions
proofmode/tactics.v
+ 1
− 3
View file @ d17a2e06
...@@ -97,8 +97,6 @@ Tactic Notation "iAssumption" := ...@@ -97,8 +97,6 @@ Tactic Notation "iAssumption" :=
(** * False *) (** * False *)
Tactic Notation "iExFalso" := apply tac_ex_falso. Tactic Notation "iExFalso" := apply tac_ex_falso.
Tactic Notation "iContradiction" constr(H) := iExFalso; iExact H.
Tactic Notation "iContradiction" := iExFalso; iAssumption.
(** * Pure introduction *) (** * Pure introduction *)
Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := Tactic Notation "iIntro" "{" simple_intropattern(x) "}" :=
...@@ -551,7 +549,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) := ...@@ -551,7 +549,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IFrame => iFrame Hz | IFrame => iFrame Hz
| IName ?y => iRename Hz into y | IName ?y => iRename Hz into y
| IPersistent ?pat => iPersistent Hz; go Hz pat | IPersistent ?pat => iPersistent Hz; go Hz pat
| IList [[]] => iContradiction Hz | IList [[]] => iExFalso; iExact Hz
| IList [[?pat1; ?pat2]] => | IList [[?pat1; ?pat2]] =>
let Hy := iFresh in iSepDestruct Hz as Hz Hy; go Hz pat1; go Hy 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] | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment