From b4a486e43547ac518ecb2190032d519246e59870 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 12 Jul 2024 13:11:26 +0200 Subject: [PATCH] Adapt to coq/coq#19362 (reduction effects take locality) also fix a deprecation warning --- redeffect.mlg.cppo | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/redeffect.mlg.cppo b/redeffect.mlg.cppo index 8c936ed..01a7171 100644 --- a/redeffect.mlg.cppo +++ b/redeffect.mlg.cppo @@ -21,7 +21,9 @@ DECLARE PLUGIN "coq-reduction-effects.plugin" { let check_ID_type env sigma typ = -#if COQ_VERSION >= (8, 18, 0) +#if COQ_VERSION >= (8, 21, 0) + let decls,_ = whd_decompose_prod env sigma typ in +#elif COQ_VERSION >= (8, 18, 0) let decls,_ = hnf_decompose_prod env sigma typ in #else let decls,_ = splay_prod env sigma typ in @@ -66,7 +68,11 @@ let _ = declare_reduction_effect printing_name printing_hook let declare_effect ref = let ref = Smartlocate.global_with_alias ref in let cst = check_valid_print_ref ref in +#if COQ_VERSION >= (8, 21, 0) + set_reduction_effect Export cst printing_name +#else set_reduction_effect cst printing_name +#endif } VERNAC COMMAND EXTEND PrintingEffect CLASSIFIED AS SIDEFF