diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b84be4600c..12a1566e20 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2197,7 +2197,8 @@ let setoid_transitivity c = (transitivity_red true c) let setoid_symmetry_in id = - Proofview.V82.tactic (fun gl -> + let open Tacmach.New in + Proofview.Goal.enter { enter = begin fun gl -> let sigma = project gl in let ctype = pf_unsafe_type_of gl (mkVar id) in let binders,concl = decompose_prod_assum sigma ctype in @@ -2211,11 +2212,10 @@ let setoid_symmetry_in id = let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in let new_hyp' = mkApp (he, [| c2 ; c1 |]) in let new_hyp = it_mkProd_or_LetIn new_hyp' binders in - Proofview.V82.of_tactic (tclTHENLAST (Tactics.assert_after_replacing id new_hyp) (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ])) - gl) + end } let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry |