aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-17 11:02:58 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-17 11:06:14 +0200
commit43343c1f79d9f373104ae5174baf41e2257e2b8d (patch)
tree7ac3a1ec228702fd8bf81c828e3d3e1c8f0ebc3c /plugins
parentcddddce068bc0482f62ffab8e412732a307b90bb (diff)
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.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml2
-rw-r--r--plugins/omega/coq_omega.ml4
2 files changed, 3 insertions, 3 deletions
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 ())