diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /theories/Init/Tactics.v | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'theories/Init/Tactics.v')
-rw-r--r-- | theories/Init/Tactics.v | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 59fdbb42..5d1e87ae 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -55,12 +55,6 @@ Ltac contradict H := | _ => (elim H;fail) || pos H end. -(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*) - -Ltac swap H := - idtac "swap is OBSOLETE: use contradict instead."; - intro; apply H; clear H. - (* To contradict an hypothesis without copying its type. *) Ltac absurd_hyp H := @@ -79,7 +73,7 @@ Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x. (* use either discriminate or injection on a hypothesis *) -Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). +Ltac destr_eq H := discriminate H || (try (injection H as H)). (* Similar variants of destruct *) |