diff options
| author | sacerdot | 2001-01-12 10:44:16 +0000 |
|---|---|---|
| committer | sacerdot | 2001-01-12 10:44:16 +0000 |
| commit | cac23bb7ed8087f78624f408b8e1f4de1cfc01f6 (patch) | |
| tree | fad9c5e3c3429cba35133229f7c31a75ae45e763 /lib | |
| parent | 2c80742b0f1d8f51a7afcf533194a092c6007fad (diff) | |
Now Ring does not perform any more the same reduction twice.
This was a logical bug of the sort_subterm function, in the
sense that the aim of the function (as stated in the comment)
was not to make early reductions mess with subterms; what
happened, though, was that the first reduction completely
removed the term and the second reduction became completely
dummy.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions