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] 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)