Stop adding interp object at link time

Author: SkySkimmer

plugin/bignums_syntax.ml

@@ -194,13 +194,17 @@ let bigN_list_of_constructors =
 let declare_numeral_interpreter uid sc dir interp (patl,uninterp,b) =
   (* unsynchronized state *)
   Notation.register_bignumeral_interpretation uid (interp,uninterp);
-  (* interp object *)
-  Notation.enable_prim_token_interpretation { pt_local = false;
-    pt_scope = sc;
-    pt_interp_info = Uid uid;
-    pt_required = dir;
-    pt_refs = patl;
-    pt_in_match = b }
+  let interp () =
+    Notation.enable_prim_token_interpretation {
+      pt_local = false;
+      pt_scope = sc;
+      pt_interp_info = Uid uid;
+      pt_required = dir;
+      pt_refs = patl;
+      pt_in_match = b;
+    }
+  in
+  Mltop.declare_cache_obj_full (CacheObj { synterp = (fun () -> ()); interp }) "coq-bignums.plugin"
 
 (* Actually declares the interpreter for bigN *)
 let () =