diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-10 11:22:23 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-10 11:22:23 +0200 |
| commit | 80b589e91fe4c6e6e390132633557dc04b9c533a (patch) | |
| tree | 57437fff190213c90152e67d8d69a104d57f23a8 /kernel/univ.mli | |
| parent | 5e7b2a59524523c0f4f4631421a35dadeebbada8 (diff) | |
Remove unused function in univ
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index fee47235a..74bd01610 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -173,7 +173,6 @@ type universes type 'a check_function = universes -> 'a -> 'a -> bool val check_leq : universe check_function val check_eq : universe check_function -val lax_check_eq : universe check_function (* same, without anomaly *) (** The empty graph of universes *) val empty_universes : universes |