Tactics API using EConstr.

1 files changed, 7 insertions, 7 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index a8be704b2..a92b14dbe 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -33,8 +33,8 @@ let absurd c =
     let t = EConstr.Unsafe.to_constr j.Environ.utj_val in
     let tac =
     Tacticals.New.tclTHENLIST [
-      elim_type (build_coq_False ());
-      Simple.apply (mk_absurd_proof t)
+      elim_type (EConstr.of_constr (build_coq_False ()));
+      Simple.apply (EConstr.of_constr (mk_absurd_proof t))
     ] in
     Sigma.Unsafe.of_pair (tac, sigma)
   end }
@@ -67,7 +67,7 @@ let contradiction_context =
           let typ = nf_evar sigma (NamedDecl.get_type d) in
 	  let typ = whd_all env sigma (EConstr.of_constr typ) in
 	  if is_empty_type sigma (EConstr.of_constr typ) then
-	    simplest_elim (mkVar id)
+	    simplest_elim (EConstr.mkVar id)
 	  else match kind_of_term typ with
 	  | Prod (na,t,u) when is_empty_type sigma (EConstr.of_constr u) ->
              let is_unit_or_eq =
@@ -82,14 +82,14 @@ let contradiction_context =
                    let params = Util.List.firstn nparams args in
                    let p = applist ((mkConstructUi (indu,1)), params) in
                    (* Checking on the fly that it type-checks *)
-                   simplest_elim (mkApp (mkVar id,[|p|]))
+                   simplest_elim (EConstr.mkApp (EConstr.mkVar id,[|EConstr.of_constr p|]))
                | None ->
                  Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type."))
 	      (Proofview.tclORELSE
                  (Proofview.Goal.enter { enter = begin fun gl ->
                    let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
 	           filter_hyp (fun typ -> is_conv_leq (EConstr.of_constr typ) (EConstr.of_constr t))
-		     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
+		     (fun id' -> simplest_elim (EConstr.mkApp (EConstr.mkVar id,[|EConstr.mkVar id'|])))
                  end })
                  begin function (e, info) -> match e with
 	           | Not_found -> seek_neg rest
@@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) =
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
-    let typ = type_of (EConstr.of_constr c) in
+    let typ = type_of c in
     let _, ccl = splay_prod env sigma (EConstr.of_constr typ) in
     if is_empty_type sigma (EConstr.of_constr ccl) then
       Tacticals.New.tclTHEN
@@ -124,7 +124,7 @@ let contradiction_term (c,lbind as cl) =
         begin
           if lbind = NoBindings then
             filter_hyp (fun c -> is_negation_of env sigma typ (EConstr.of_constr c))
-              (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
+              (fun id -> simplest_elim (EConstr.mkApp (EConstr.mkVar id,[|c|])))
           else
             Proofview.tclZERO Not_found
         end