4 files changed, 16 insertions, 17 deletions
diff --git a/library/dune b/library/dune
index 344fad5a75..bf90511ead 100644
--- a/library/dune
+++ b/library/dune
@@ -1,9 +1,9 @@
 (library
  (name library)
  (synopsis "Coq's Loadable Libraries (vo) Support")
- (public_name coq.library)
+ (public_name coq-core.library)
  (wrapped false)
  (libraries kernel))
 
 (documentation
- (package coq))
+ (package coq-core))
diff --git a/library/nametab.ml b/library/nametab.ml
index e94b696b60..bd96446f1c 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -574,7 +574,7 @@ let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as exn ->
     let exn, info = Exninfo.capture exn in
-    if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found");
+    if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str "pr_global_env not found");
     Exninfo.iraise (exn, info)
 
 let global_inductive qid =
diff --git a/library/summary.ml b/library/summary.ml
index 221ac868fa..572467ada3 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -131,28 +131,27 @@ let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x
 
 module Local = struct
 
-type 'a local_ref = ('a CEphemeron.key * 'a Dyn.tag) ref
+type 'a local_ref = 'a CEphemeron.key ref * 'a CEphemeron.key Dyn.tag
 
-let set r v = r := (CEphemeron.create v, snd !r)
+let set (r, tag) v = r := CEphemeron.create v
 
-let get r =
-  let key, name = !r in
-  try CEphemeron.get key
+let get (key, name) =
+  try CEphemeron.get !key
   with CEphemeron.InvalidKey ->
     let { init_function } = DynMap.find name !sum_map in
     init_function ();
-    CEphemeron.get (fst !r)
+    CEphemeron.get !key
 
-let ref ?(freeze=fun x -> x) ~name init =
+let ref (type a) ~name (init : a) : a local_ref =
   let () = check_name (mangle name) in
-  let tag : 'a Dyn.tag = Dyn.create (mangle name) in
-  let r = pervasives_ref (CEphemeron.create init, tag) in
+  let tag : a CEphemeron.key Dyn.tag = Dyn.create (mangle name) in
+  let r = pervasives_ref (CEphemeron.create init) in
   let () = sum_map := DynMap.add tag
-    { freeze_function = (fun ~marshallable -> freeze (get r));
-      unfreeze_function = (set r);
-      init_function = (fun () -> set r init) } !sum_map
+    { freeze_function = (fun ~marshallable -> !r);
+      unfreeze_function = (fun v -> r := v);
+      init_function = (fun () -> r := CEphemeron.create init) } !sum_map
   in
-  r
+  (r, tag)
 
 let (!) = get
 let (:=) = set
diff --git a/library/summary.mli b/library/summary.mli
index 7c5e1bee6f..a6f94a49ae 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -53,7 +53,7 @@ val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a
 module Local : sig
 
   type 'a local_ref
-  val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref
+  val ref : name:string -> 'a -> 'a local_ref
   val (:=) : 'a local_ref -> 'a -> unit
   val (!) : 'a local_ref -> 'a