From ef8cf82668a794f116ae714749f434e3505880d1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 29 May 2017 18:34:47 +0200 Subject: tactics cleanup: remove constr_of_global calls --- tactics/contradiction.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'tactics/contradiction.ml') 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 } -- cgit v1.2.3