From efa3add0c03b70ecda3890cc6c69e66850605e7d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 Jun 2014 19:06:03 +0200
Subject: Fix handling of side effects in Defined objects (Closes: HoTT#111 +
 3344)

Every time you use abstract a kitten dies, please stop.
---
 kernel/declareops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 149eeba287..51b7b6f971 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -284,7 +284,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 = CList.uniquize l
+let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l))
 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