From cac23bb7ed8087f78624f408b8e1f4de1cfc01f6 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 12 Jan 2001 10:44:16 +0000
Subject: 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
---
 contrib/ring/quote.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'contrib')

diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 666d15dee2..ed93a13dc4 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 
-- 
cgit v1.2.3