tactics cleanup: remove constr_of_global calls

1 files changed, 6 insertions, 5 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index fe44559ed..5e7090ded 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -19,10 +19,9 @@ module NamedDecl = Context.Named.Declaration
 
 (* Absurd *)
 
-let mk_absurd_proof t =
-  let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in
+let mk_absurd_proof coq_not t =
   let id = Namegen.default_dependent_ident in
-  mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]),
+  mkLambda (Names.Name id,mkApp(coq_not,[|t|]),
     mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
 
 let absurd c =
@@ -34,9 +33,11 @@ let absurd c =
     let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
     let t = j.Environ.utj_val in
     let tac =
+    Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot ->
+    Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse ->
     Tacticals.New.tclTHENLIST [
-      elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()));
-      Simple.apply (mk_absurd_proof t)
+      elim_type coqfalse;
+      Simple.apply (mk_absurd_proof coqnot t)
     ] in
     Sigma.Unsafe.of_pair (tac, sigma)
   end }