diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-12 10:44:16 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-12 10:44:16 +0000 |
| commit | cac23bb7ed8087f78624f408b8e1f4de1cfc01f6 (patch) | |
| tree | fad9c5e3c3429cba35133229f7c31a75ae45e763 /contrib | |
| 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 'contrib')
| -rw-r--r-- | contrib/ring/quote.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 666d15dee..ed93a13dc 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -354,6 +354,7 @@ let rec subterm gl (t : constr) (t' : constr) = let rec sort_subterm gl l = let rec insert c = function | [] -> [c] + | (h::t as l) when c = h -> l (* Avoid doing the same work twice *) | h::t -> if subterm gl c h then c::h::t else h::(insert c t) in match l with |