diff options
| author | jforest | 2011-09-09 15:20:15 +0000 |
|---|---|---|
| committer | jforest | 2011-09-09 15:20:15 +0000 |
| commit | 0c0481a2fdea2e5efb30d9cd11563e04c2861077 (patch) | |
| tree | e409b9e89285e3c5868fc6d27e6c1c28d51eb484 /plugins/funind/invfun.ml | |
| parent | 3b4a94e3b7b827fe8f66d6c50a09439b07b594db (diff) | |
correction du bug 2047
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14465 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |