diff options
| author | herbelin | 2011-12-06 11:37:37 +0000 |
|---|---|---|
| committer | herbelin | 2011-12-06 11:37:37 +0000 |
| commit | c4d9efb1d6cca48fd33764fa1f17172d86b13e78 (patch) | |
| tree | 75c96ab233f8dbcbd5e168c32a45d2f14aa491a2 | |
| parent | 81429f879fa76ac24c25d89a6ada2073ea8361e2 (diff) | |
Backtrack on synchronizing universe counter with reset
mechanism, section discharge is not ready for that.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14765 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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)) |