From f076842930dd1e1ba2d27e71f76f1c35113203e0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 15 Jul 2025 13:26:53 +0200 Subject: [PATCH 1/2] move declare_scope call into declare_numeral_interpreter and add staging comments --- plugin/bignums_syntax.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/plugin/bignums_syntax.ml b/plugin/bignums_syntax.ml index a46a0c8..804a9ed 100644 --- a/plugin/bignums_syntax.ml +++ b/plugin/bignums_syntax.ml @@ -192,9 +192,12 @@ let bigN_list_of_constructors = build 0 let declare_numeral_interpreter uid sc dir interp (patl,uninterp,b) = - let open Notation in - register_bignumeral_interpretation uid (interp,uninterp); - enable_prim_token_interpretation { pt_local = false; + (* interp summary, no object *) + Notation.declare_scope sc; + (* 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; @@ -203,7 +206,6 @@ let declare_numeral_interpreter uid sc dir interp (patl,uninterp,b) = (* Actually declares the interpreter for bigN *) let () = - Notation.declare_scope bigN_scope; declare_numeral_interpreter "bignums.bigN" bigN_scope (bigN_path, bigN_module) interp_bigN @@ -241,7 +243,6 @@ let uninterp_bigZ (AnyGlobConstr rc) = (* Actually declares the interpreter for bigZ *) let () = - Notation.declare_scope bigZ_scope; declare_numeral_interpreter "bignums.bigZ" bigZ_scope (bigZ_path, bigZ_module) interp_bigZ @@ -263,7 +264,6 @@ let uninterp_bigQ (AnyGlobConstr rc) = (* Actually declares the interpreter for bigQ *) let () = - Notation.declare_scope bigQ_scope; declare_numeral_interpreter "bignums.bigQ" bigQ_scope (bigQ_path, bigQ_module) interp_bigQ From 889f675c44efabe9ce119ab774460e6a860a98ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 15 Jul 2025 13:37:40 +0200 Subject: [PATCH 2/2] Stop adding interp object at link time --- plugin/bignums_syntax.ml | 31 ++++++++++++++++++++++--------- 1 file changed, 22 insertions(+), 9 deletions(-) diff --git a/plugin/bignums_syntax.ml b/plugin/bignums_syntax.ml index 804a9ed..7db0172 100644 --- a/plugin/bignums_syntax.ml +++ b/plugin/bignums_syntax.ml @@ -191,18 +191,31 @@ let bigN_list_of_constructors = in build 0 +let cache_bignums o = + Notation.declare_scope o.Notation.pt_scope; + Notation.enable_prim_token_interpretation o + +let bignums_obj = + Libobject.declare_object @@ + Libobject.superglobal_object_nodischarge "bignums_obj" + ~cache:cache_bignums + ~subst:None + let declare_numeral_interpreter uid sc dir interp (patl,uninterp,b) = - (* interp summary, no object *) - Notation.declare_scope sc; (* 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 () = Lib.add_leaf (bignums_obj { + (* we wrap in out own object (to get superglobal instead of export), + so we pass local to the Notation layer *) + pt_local = true; + 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 () =