From d6f8e6e6c2cebac339d1dd1e48bfe0d9dbe95e9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 16 Jul 2025 13:10:37 +0200 Subject: [PATCH] Adapt to rocq-prover/rocq#20911 (Notation.prim_token_uid is private) --- plugin/bignums_syntax.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugin/bignums_syntax.ml b/plugin/bignums_syntax.ml index 7db0172..990008d 100644 --- a/plugin/bignums_syntax.ml +++ b/plugin/bignums_syntax.ml @@ -203,7 +203,7 @@ let bignums_obj = let declare_numeral_interpreter uid sc dir interp (patl,uninterp,b) = (* unsynchronized state *) - Notation.register_bignumeral_interpretation uid (interp,uninterp); + let uid = Notation.register_bignumeral_interpretation uid (interp,uninterp) in 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 *)