diff options
| author | herbelin | 2011-12-05 22:33:28 +0000 |
|---|---|---|
| committer | herbelin | 2011-12-05 22:33:28 +0000 |
| commit | 81429f879fa76ac24c25d89a6ada2073ea8361e2 (patch) | |
| tree | 1356e28b029cad322461a7736e702827541f7bed /pretyping/termops.ml | |
| parent | 223429a0fe7de02ab4e495529b795f5733d6dd32 (diff) | |
Registering universe and meta/evar counters as summaries so as to
eventually get the same numbers when replaying (but does not work for
Undo/Abort which are still not plugged to the summary freezing
mechanism).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14764 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 2662093487..67d2a489ac 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -148,9 +148,14 @@ 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)) + let new_univ () = Univ.make_universe (new_univ_level ()) let new_Type () = mkType (new_univ ()) let new_Type_sort () = Type (new_univ ()) |