Extension de l'utilisation de contradiction

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

4 files changed, 19 insertions, 17 deletions

diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 3139db208..8da7530ea 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -609,7 +609,7 @@ let rec fourier gl=
 				]));
                        !tac1]);
 	   tac:=(tclTHENS (cut (get coq_False))
-				  [tclTHEN intro contradiction;
+				  [tclTHEN intro (contradiction None);
 				   !tac])
       |_-> assert false) |_-> assert false
 	  );
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index ab7f0c550..a6d4296b7 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -17,6 +17,7 @@ open Tacticals
 open Tactics
 open Coqlib
 open Reductionops
+open Rawterm
 
 (* Absurd *)
 
@@ -61,26 +62,27 @@ let contradiction_context gl =
 	  | _ -> seek_neg rest gl in
   seek_neg (pf_hyps gl) gl
 
-let contradiction = tclTHEN intros contradiction_context
-
 let is_negation_of env sigma typ t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
     | Prod (na,t,u) -> is_empty_type u & is_conv_leq env sigma typ t
     | _ -> false
 
-let contradiction_term c gl =
+let contradiction_term (c,lbind as cl) gl =
   let env = pf_env gl in
   let sigma = project gl in
   let typ = pf_type_of gl c in
-  if is_empty_type typ then
-    simplest_elim c gl
+  let _, ccl = splay_prod env sigma typ in
+  if is_empty_type ccl then
+    tclTHEN (elim cl None) (tclTRY assumption) gl
   else
     try
-      (match kind_of_term (whd_betadeltaiota env sigma typ) with
-	| Prod (na,t,u) when is_empty_type u ->
-	    filter_hyp (fun typ -> pf_conv_x_leq gl typ t)
-	    (fun id -> simplest_elim (mkApp (c,[|mkVar id|]))) gl
-	| _ ->
-	    filter_hyp (is_negation_of env sigma typ)
-	    (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) gl)
+      if lbind = NoBindings then
+	filter_hyp (is_negation_of env sigma typ)
+	  (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) gl
+      else
+	raise Not_found
     with Not_found -> error "Not a contradiction"
+
+let contradiction = function
+  | None -> tclTHEN intros contradiction_context
+  | Some c -> contradiction_term c
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 27b926d7a..65961d988 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -12,8 +12,8 @@
 open Names
 open Term
 open Proof_type
+open Rawterm
 (*i*)
 
-val absurd                      : constr     -> tactic
-val contradiction_on_hyp        : identifier -> tactic
-val contradiction               : tactic
+val absurd                      : constr -> tactic
+val contradiction               : constr with_bindings option -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f783b17d5..6f87f1016 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -107,7 +107,7 @@ TACTIC EXTEND Absurd
 END
 
 TACTIC EXTEND Contradiction
- [ "Contradiction" ] -> [ contradiction ]
+ [ "Contradiction" constr_with_bindings_opt(c) ] -> [ contradiction c ]
 END
 
 (* AutoRewrite *)