small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is

more general.



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

1 files changed, 10 insertions, 10 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 29ec5f888..de38e88c1 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -49,23 +49,23 @@ Ltac contradict name :=
           end
      end).
 
-(* to contradict an hypothesis without copying its type. *)
+(* 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 := 
-  (* idtac "absurd_hyp is OBSOLETE: use contradict instead."; *)
+  idtac "contradict is OBSOLETE: use contradict instead.";
   let T := type of h in 
   absurd T.
 
-(* A useful complement to absurd_hyp. Here t : ~ A where H : A. *)
-Ltac false_hyp H t :=
-absurd_hyp H; [apply t | assumption].
-
-(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
+(* A useful complement to contradict. Here t : ~ A where H : A. *)
 
-Ltac swap H := 
-  (* idtac "swap is OBSOLETE: use contradict instead."; *)
-  intro; apply H; clear H.
+Ltac false_hyp h t := 
+  let T := type of h in absurd T; [ apply t | assumption ].
 
 (* A case with no loss of information. *)