contradict can now handle False hypothesis in the spirit of contradiction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10771 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 2 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 50653c420..d822a45c5 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -18,6 +18,7 @@ Require Import Logic.
     -   H:~A |- ~B    gives  H: B |-  A
     -   H: A |-  B    gives       |- ~A
     -   H: A |- ~B    gives  H: B |- ~A
+    -   H:False leads to a resolved subgoal.
    Moreover, negations may be in unfolded forms, 
    and A or B may live in Type *)
 
@@ -46,7 +47,7 @@ Ltac contradict H :=
   match type of H with 
    | (~_) => neg H
    | (_->False) => neg H
-   | _ => pos H
+   | _ => (elim H;fail) || pos H
   end.
 
 (* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
@@ -62,7 +63,7 @@ Ltac absurd_hyp H :=
   let T := type of H in 
   absurd T.
 
-(* A useful complement to contradict. Here H : A and G allows to conclude ~A *)
+(* A useful complement to contradict. Here H:A while G allows to conclude ~A *)
 
 Ltac false_hyp H G := 
   let T := type of H in absurd T; [ apply G | assumption ].