From d59999a46b5e233162cf781cea206558c80257c5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 17 Jan 2025 16:27:41 +0100 Subject: [PATCH] Adapt to coq/coq#19985 (template poly has pseudo sort poly) --- src/coq_elpi_HOAS.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index a6cf116b7..39b64f4d1 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -2993,7 +2993,7 @@ let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~fin } in let env_ar = Environ.pop_rel_context (List.length ctx_params) env_ar_params in - ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags ~env_ar ~ctx_params + ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly ()] ~flags ~env_ar ~ctx_params [%%endif]