diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
2 files changed, 3 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 572d4b7ab7..12d31d0f31 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 24aca2a689..df41951c32 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 |