diff options
| -rw-r--r-- | pretyping/termops.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 67d2a489ac..aaeb172c9b 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -148,10 +148,6 @@ let set_module m = current_module := m*) let new_univ_level = let univ_gen = ref 0 in - Summary.declare_summary "Universe counter" - { Summary.freeze_function = (fun () -> !univ_gen); - Summary.unfreeze_function = (fun n -> univ_gen := n); - Summary.init_function = (fun () -> univ_gen := 0) }; (fun sp -> incr univ_gen; Univ.make_universe_level (Lib.library_dp(),!univ_gen)) |