From 96f8d358c7d3c9a08ff2006f42716bc64937dad2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 3 Mar 2014 14:20:42 +0100
Subject: Fixing pervasive equalities. In particular, I removed the code that
 deleted duplicates in kernel side effects. They were chosen according to an
 equality that was quite irrelevant, and as expected this patch did not break
 the test-suite.

---
 kernel/declareops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 7c852a7556..1b67de0eaa 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -248,7 +248,7 @@ type side_effects = side_effect list
 let no_seff = ([] : side_effects)
 let iter_side_effects f l = List.iter f (List.rev l)
 let fold_side_effects f a l = List.fold_left f a l
-let uniquize_side_effects l = List.uniquize l
+let uniquize_side_effects l = l (** FIXME: there is something dubious here *)
 let union_side_effects l1 l2 = l1 @ l2
 let flatten_side_effects l = List.flatten l
 let side_effects_of_list l = l
-- 
cgit v1.2.3