diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-24 17:24:46 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-24 17:41:21 +0200 |
commit | 6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 (patch) | |
tree | b8a60ea2387f14a415d53a3cd9db516e384a5b4f /plugins/ltac/rewrite.ml | |
parent | a02f76f38592fd84cabd34102d38412f046f0d1b (diff) | |
parent | 28f8da9489463b166391416de86420c15976522f (diff) |
Merge branch 'trunk' into located_switch
Diffstat (limited to 'plugins/ltac/rewrite.ml')
-rw-r--r-- | plugins/ltac/rewrite.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2ef435b6b..e8c9f4eba 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -17,7 +17,6 @@ open EConstr open Vars open Reduction open Tacticals.New -open Tacmach open Tactics open Pretype_errors open Typeclasses @@ -39,7 +38,7 @@ open Proofview.Notations open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -module RelDecl = Context.Rel.Declaration +(* module RelDecl = Context.Rel.Declaration *) (** Typeclass-based generalized rewriting. *) @@ -2196,7 +2195,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 @@ -2210,11 +2210,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 |