diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-04 22:11:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-04 22:11:06 +0200 |
| commit | f9b33f4bc396eaf60abaaee270b4701fe05d82f4 (patch) | |
| tree | 0b26e6be2a8cd089add5508f3bf5afa77ad5ef8d /kernel/univ.ml | |
| parent | 5bba0c3f300f67f402cd8be1801cbb36e4652265 (diff) | |
Fixing semantics of Univ.Level.equal.
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 2fd94e1a9..86aebbce9 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 = |