From f66b37418845d663db318567270e2108bc323d45 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 28 Mar 2023 15:34:22 +0200 Subject: [PATCH] Adapt to coq/coq#16967 (increased kerpair checking) --- template-coq/src/plugin_core.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml index 453294769..a67bafb83 100644 --- a/template-coq/src/plugin_core.ml +++ b/template-coq/src/plugin_core.ml @@ -187,7 +187,7 @@ let quote_module (qualid : qualid) : global_reference list = match me with | Abstract -> [] | Algebraic _ -> [] - | Struct s -> get_refs (Modops.annotate_struct_body s mb.Declarations.mod_type) + | Struct (reso,s) -> get_refs (Modops.annotate_struct_body s mb.Declarations.mod_type) | FullStruct -> get_refs mb.Declarations.mod_type in aux mb