diff options
Diffstat (limited to 'contrib/ring/quote.ml')
| -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 |