4 files changed, 31 insertions, 6 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 062196b39..fe872db8b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -893,7 +893,7 @@ let sort_universes orig =
 (* Temporary inductive type levels *)
 
 let fresh_local_univ, set_remote_fresh_local_univ =
-  RemoteCounter.new_counter 0 ~incr:((+) 1)
+  RemoteCounter.new_counter ~name:"local_univ" 0 ~incr:((+) 1)
     ~build:(fun n -> Atom (UniverseLevel.Level (n, Names.DirPath.empty)))
 
 (* Miscellaneous functions to remove or test local univ assumed to
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index e0e2d5cbc..bec46901f 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -9,8 +9,16 @@
 type 'a getter = unit -> 'a
 type 'a installer = ('a getter) -> unit
 
-let new_counter a ~incr ~build =
-  let data = ref a in
+type remote_counters_status = (string * Obj.t) list
+
+let counters : remote_counters_status ref = ref []
+
+let (!!) x = !(!x)
+
+let new_counter ~name a ~incr ~build =
+  assert(not (List.mem_assoc name !counters));
+  let data = ref (ref a) in
+  counters := (name, Obj.repr data) :: !counters;
   let m = Mutex.create () in
   let mk_thsafe_getter f () =
     (* - slaves must use a remote counter getter, not this one! *)
@@ -22,7 +30,7 @@ let new_counter a ~incr ~build =
     | _ -> ());
     Mutex.lock m; let x = f () in Mutex.unlock m;
     build x in
-  let getter = ref (mk_thsafe_getter (fun () -> data := incr !data; !data)) in
+  let getter = ref(mk_thsafe_getter (fun () -> !data := incr !!data; !!data)) in
   let installer f =
     (match !Flags.async_proofs_mode with
     | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 -> 
@@ -31,3 +39,11 @@ let new_counter a ~incr ~build =
     getter := f in
   (fun () -> !getter ()), installer
 
+let backup () = !counters
+
+let restore l =
+  List.iter (fun (name, data) ->
+    assert(List.mem_assoc name !counters);
+    let dataref = Obj.obj (List.assoc name !counters) in
+    !dataref := !!(Obj.obj data))
+  l
diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli
index f17f1be3c..5a47ba663 100644
--- a/lib/remoteCounter.mli
+++ b/lib/remoteCounter.mli
@@ -6,9 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Remote counters are *global* counters for fresh ids.  In the master/slave
+ * scenario, the slave installs a getter that asks the master for a fresh
+ * value.  In the scenario of a slave that runs after the death of the master
+ * on some marshalled data, a backup of all counters status should be taken and
+ * restored to avoid reusing ids. *)
+
 type 'a getter = unit -> 'a
 type 'a installer = ('a getter) -> unit
 
-val new_counter :
+val new_counter : name:string ->
   'a -> incr:('a -> 'a) -> build:('a -> 'b) -> 'b getter * 'b installer
 
+type remote_counters_status
+val backup : unit -> remote_counters_status
+val restore : remote_counters_status -> unit
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 781bd599c..6972f307b 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -150,7 +150,7 @@ let print_env env =
 let set_module m = current_module := m*)
 
 let new_univ_level, set_remote_new_univ_level =
-  RemoteCounter.new_counter 0 ~incr:((+) 1)
+  RemoteCounter.new_counter ~name:"univ_level" 0 ~incr:((+) 1)
     ~build:(fun n -> Univ.UniverseLevel.make (Lib.library_dp()) n)
 
 let new_univ () = Univ.Universe.make (new_univ_level ())