Using non-normalized goals in tactic interpretation.

1 files changed, 10 insertions, 6 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 13c188c79..9c8412454 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -38,30 +38,32 @@ let absurd c = Proofview.V82.tactic (absurd c)
 
 (* Contradiction *)
 
+(** [f] does not assume its argument to be [nf_evar]-ed. *)
 let filter_hyp f tac =
   let rec seek = function
     | [] -> Proofview.tclZERO Not_found
     | (id,_,t)::rest when f t -> tac id
     | _::rest -> seek rest in
-  Proofview.Goal.enter begin fun gl ->
-    let hyps = Proofview.Goal.hyps gl in
+  Proofview.Goal.raw_enter begin fun gl ->
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     seek hyps
   end
 
 let contradiction_context =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let rec seek_neg l = match l with
       | [] ->  Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
       | (id,_,typ)::rest ->
+          let typ = nf_evar sigma typ in
 	  let typ = whd_betadeltaiota env sigma typ in
 	  if is_empty_type typ then
 	    simplest_elim (mkVar id)
 	  else match kind_of_term typ with
 	  | Prod (na,t,u) when is_empty_type u ->
 	      (Proofview.tclORELSE
-                 (Proofview.Goal.enter begin fun gl ->
+                 (Proofview.Goal.raw_enter begin fun gl ->
                    let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
 	           filter_hyp (fun typ -> is_conv_leq typ t)
 		     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
@@ -72,13 +74,15 @@ let contradiction_context =
                  end)
 	  | _ -> seek_neg rest
     in
-    let hyps = Proofview.Goal.hyps gl in
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     seek_neg hyps
   end
 
 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
+    | Prod (na,t,u) ->
+      let u = nf_evar sigma u in
+      is_empty_type u && is_conv_leq env sigma typ t
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =