diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 2e3b6e1af7..9934e3a00a 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1833,7 +1833,7 @@ 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 - Tacticals.New.tclTHENS (Proofview.V82.tactic (Tactics.cut new_hyp)) + Tacticals.New.tclTHENS (Tactics.cut new_hyp) [ Proofview.V82.tactic (intro_replacing id); Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Tactics.assumption ] ] end |