diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 359738fd58..4917c64f41 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -504,6 +504,24 @@ 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 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 |