From b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 8 Oct 2015 16:00:06 +0200
Subject: Univs: fix bug #3807

Add a flag to disallow minimization to set
---
 kernel/univ.ml  | 3 +++
 kernel/univ.mli | 1 +
 2 files changed, 4 insertions(+)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 34eb283d73..c0bd3bacd7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1797,6 +1797,9 @@ struct
   let empty = (LSet.empty, Constraint.empty)
   let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
 
+  let equal (univs, cst as x) (univs', cst' as y) =
+    x == y || (LSet.equal univs univs' && Constraint.equal cst cst')
+									
   let of_set s = (s, Constraint.empty)
   let singleton l = of_set (LSet.singleton l)
   let of_instance i = of_set (Instance.levels i)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4cc8a2528f..cbaf7e546a 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -360,6 +360,7 @@ sig
   val of_instance : Instance.t -> t
   val of_set : universe_set -> t
 
+  val equal : t -> t -> bool
   val union : t -> t -> t
 
   val append : t -> t -> t
-- 
cgit v1.2.3