diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/invfun.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 4917c64f41..0b04a572fe 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -513,15 +513,6 @@ and intros_with_rewrite_aux : tactic = intros_with_rewrite ] g - else if isVar args.(2) - then - let id = pf_get_new_id (id_of_string "y") g in - tclTHENSEQ [ h_intro id; - generalize_dependent_of (destVar args.(2)) id; - tclTRY (Equality.rewriteRL (mkVar id)); - intros_with_rewrite - ] - g else begin let id = pf_get_new_id (id_of_string "y") g in |