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 | |
| 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.
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
4 files changed, 6 insertions, 7 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 ()) diff --git a/tactics/equality.ml b/tactics/equality.ml index 572d4b7ab..12d31d0f3 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -974,7 +974,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS eff <*> tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))] + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1316,7 +1316,7 @@ let inject_if_homogenous_dependent_pair ty = onLastHyp (fun hyp -> tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar hyp]; - Proofview.V82.tactic (refine + Proofview.V82.tactic (Tacmach.refine (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) ])] with Exit -> @@ -1362,7 +1362,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; - Proofview.V82.tactic (refine pf)]) + Proofview.V82.tactic (Tacmach.refine pf)]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 24aca2a68..df41951c3 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -30,7 +30,6 @@ val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) val introduction : ?check:bool -> Id.t -> unit Proofview.tactic -val refine : constr -> tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic |