diff options
| -rw-r--r-- | kernel/univ.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 44d487c1a5..062196b395 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -892,10 +892,6 @@ let sort_universes orig = (* Temporary inductive type levels *) -let fresh_level = - let n = ref 0 in - fun () -> incr n; UniverseLevel.Level (!n, Names.DirPath.empty) - let fresh_local_univ, set_remote_fresh_local_univ = RemoteCounter.new_counter 0 ~incr:((+) 1) ~build:(fun n -> Atom (UniverseLevel.Level (n, Names.DirPath.empty))) |