From f9b33f4bc396eaf60abaaee270b4701fe05d82f4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Aug 2014 22:11:06 +0200
Subject: Fixing semantics of Univ.Level.equal.

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

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 2fd94e1a94..86aebbce93 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -265,7 +265,7 @@ struct
       | Set, Set -> true
       | Level (n,d), Level (n',d') ->
         Int.equal n n' && DirPath.equal d d'
-      | Var n, Var n' -> true
+      | Var n, Var n' -> Int.equal n n'
       | _ -> false
 
   let compare u v =
-- 
cgit v1.2.3