From 472705a38b6f0308f8bcff7880e0eba0480a13c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 13 Feb 2024 14:09:15 +0100 Subject: [PATCH 1/2] Fix compilation on Coq master. --- 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 568b91b..bc49902 100644 --- a/plugin/bignums_syntax.ml +++ b/plugin/bignums_syntax.ml @@ -198,7 +198,7 @@ let bigN_list_of_constructors = let declare_numeral_interpreter uid sc dir interp (patl,uninterp,b) = let open Notation in register_bignumeral_interpretation uid (interp,uninterp); - { pt_local = false; + enable_prim_token_interpretation { pt_local = false; pt_scope = sc; pt_interp_info = Uid uid; pt_required = dir; From c5bde2b880ea1508d7ff15c2d283aad046ace744 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 13 Feb 2024 14:17:22 +0100 Subject: [PATCH 2/2] Harden a bit the plugin implementation. We check that the returned value of effectful calls is indeed unit. --- plugin/bignums_syntax.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/plugin/bignums_syntax.ml b/plugin/bignums_syntax.ml index bc49902..cd0cd32 100644 --- a/plugin/bignums_syntax.ml +++ b/plugin/bignums_syntax.ml @@ -206,7 +206,7 @@ let declare_numeral_interpreter uid sc dir interp (patl,uninterp,b) = pt_in_match = b } (* Actually declares the interpreter for bigN *) -let _ = +let () = Notation.declare_scope bigN_scope; declare_numeral_interpreter "bignums.bigN" bigN_scope (bigN_path, bigN_module) @@ -244,7 +244,7 @@ let uninterp_bigZ (AnyGlobConstr rc) = None (* Actually declares the interpreter for bigZ *) -let _ = +let () = Notation.declare_scope bigZ_scope; declare_numeral_interpreter "bignums.bigZ" bigZ_scope (bigZ_path, bigZ_module) @@ -266,7 +266,7 @@ let uninterp_bigQ (AnyGlobConstr rc) = with Non_closed -> None (* Actually declares the interpreter for bigQ *) -let _ = +let () = Notation.declare_scope bigQ_scope; declare_numeral_interpreter "bignums.bigQ" bigQ_scope (bigQ_path, bigQ_module)