From 43343c1f79d9f373104ae5174baf41e2257e2b8d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 May 2016 11:02:58 +0200 Subject: Removing the old refine tactic from the Tactics module. It is indeed confusing, as it has little to do with the proper refine defined in the New submodule. Legacy code relying on it should call the Logic or Tacmach modules instead. --- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/omega/coq_omega.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index de06af005..be6ce59bd 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -485,7 +485,7 @@ let thus_tac c ctyp submetas gls = Proofview.V82.of_tactic (exact_check proof) gls else let refiner = concl_refiner list proof gls in - Tactics.refine refiner gls + Tacmach.refine refiner gls (* general forward step *) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ab33a5d2c..0bf30e7fd 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -150,7 +150,7 @@ let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) let generalize_tac t = generalize t let elim t = simplest_elim t -let exact t = Tactics.refine t +let exact t = Tacmach.refine t let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let rev_assoc k = @@ -1847,7 +1847,7 @@ let destructure_goal = try let dec = decidability t in Tacticals.New.tclTHEN - (Proofview.V82.tactic (Tactics.refine + (Proofview.V82.tactic (Tacmach.refine (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))) intro with Undecidable -> Tactics.elim_type (build_coq_False ()) -- cgit v1.2.3