diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-17 11:02:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-17 11:06:14 +0200 |
| commit | 43343c1f79d9f373104ae5174baf41e2257e2b8d (patch) | |
| tree | 7ac3a1ec228702fd8bf81c828e3d3e1c8f0ebc3c /plugins/omega | |
| parent | cddddce068bc0482f62ffab8e412732a307b90bb (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/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 ()) |