diff options
| author | Pierre-Marie Pédrot | 2018-11-21 13:03:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-21 13:03:27 +0100 |
| commit | 4d0fea2ededb11d79f4f1abcc1595f9cec20d6dd (patch) | |
| tree | bbd47886f4649999ecad9f21ffb6ff55869f0132 /tactics/equality.ml | |
| parent | 968be14b3788e112425eedf696f2e5e35d35ba17 (diff) | |
| parent | 417641e48129c9ba8656c622c9b64cd32641e7de (diff) | |
Merge PR #8998: [legacy proof engine] Remove some cruft.
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 969f539d1f..b8967775bf 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1028,7 +1028,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1354,8 +1354,8 @@ let inject_if_homogenous_dependent_pair ty = tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar sigma hyp]; Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 -> - Proofview.V82.tactic (Tacmach.refine - (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) + Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr + (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))) ])] with Exit -> Proofview.tclUNIT () @@ -1400,7 +1400,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 (Tacmach.refine pf)]) + Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) |