From c4d9efb1d6cca48fd33764fa1f17172d86b13e78 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 6 Dec 2011 11:37:37 +0000
Subject: 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
---
 pretyping/termops.ml | 4 ----
 1 file changed, 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))
-- 
cgit v1.2.3