From a9b9049800ebb3abe0cb2ca5bad9b2060d211cb2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 May 2002 10:48:13 +0000
Subject: Pour les tactiques dépendant de False

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2718 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/contradiction.ml | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 tactics/contradiction.ml

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
new file mode 100644
index 0000000000..58b85297f0
--- /dev/null
+++ b/tactics/contradiction.ml
@@ -0,0 +1,34 @@
+open Util
+open Term
+open Proof_type
+open Hipattern
+open Tacmach
+open Tacticals
+open Tactics
+open Coqlib
+
+(* Contradiction *)
+
+let contradiction_on_hyp id gl =
+  let hyp = pf_get_hyp_typ gl id in
+  if is_empty_type hyp then
+    simplest_elim (mkVar id) gl
+  else 
+    error "Not a contradiction"
+
+(* Absurd *)
+let absurd c gls =
+  (tclTHENS
+     (tclTHEN (elim_type (build_coq_False ())) (cut c)) 
+     ([(tclTHENS
+          (cut (applist(build_coq_not (),[c]))) 
+	  ([(tclTHEN intros
+	       ((fun gl ->
+		   let ida = pf_nth_hyp_id gl 1
+                   and idna = pf_nth_hyp_id gl 2 in
+                   exact_no_check (applist(mkVar idna,[mkVar ida])) gl)));
+            tclIDTAC]));
+       tclIDTAC])) gls
+
+let contradiction gls = 
+  tclTHENLIST [ intros; elim_type (build_coq_False ()); assumption ] gls
-- 
cgit v1.2.3