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 | |
| 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
| -rw-r--r-- | pretyping/evarutil.ml | 8 | ||||
| -rw-r--r-- | pretyping/termops.ml | 5 |
2 files changed, 13 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index fecfff7a58..bf4c18f918 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -78,6 +78,10 @@ let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd (* Generator of metavariables *) let new_meta = let meta_ctr = ref 0 in + Summary.declare_summary "meta counter" + { Summary.freeze_function = (fun () -> !meta_ctr); + Summary.unfreeze_function = (fun n -> meta_ctr := n); + Summary.init_function = (fun () -> meta_ctr := 0) }; fun () -> incr meta_ctr; !meta_ctr let mk_new_meta () = mkMeta(new_meta()) @@ -144,6 +148,10 @@ let non_instantiated sigma = (* Generator of existential names *) let new_untyped_evar = let evar_ctr = ref 0 in + Summary.declare_summary "evar counter" + { Summary.freeze_function = (fun () -> !evar_ctr); + Summary.unfreeze_function = (fun n -> evar_ctr := n); + Summary.init_function = (fun () -> evar_ctr := 0) }; fun () -> incr evar_ctr; existential_of_int !evar_ctr (*------------------------------------* 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 ()) |