Bug fixed (reported by Roland): the setoire_rewrite in tactic did not work

in the followin case:

 H : t < c1
 H0: c1 < c2
=============
    t'

setoid_rewrite H0 in H

Explanation: the tactic made a cut with

H0: c1 < c2
===============
  t < c2

and then did setoid_rewrite <- H0 in H.
If c2 occurs in t, then the tactic may fail (due to wrong variance).

The simple fix consists in changing "t < c2" to "let H := c2 in t{H/c2} < c2"
and then perform an intro before proceeding.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6601 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions