diff options
| author | sacerdot | 2005-01-17 14:49:55 +0000 |
|---|---|---|
| committer | sacerdot | 2005-01-17 14:49:55 +0000 |
| commit | fe0885afe58a9c7d181ee0350513c6f22c8b7853 (patch) | |
| tree | e8bbfcf53f11c127cfb8796d167ad5669d5aa2fd /dev/objects.el | |
| parent | 1e790c56dac86ad8c637350a74a165a26709f7e3 (diff) | |
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
Diffstat (limited to 'dev/objects.el')
0 files changed, 0 insertions, 0 deletions