Adapt to coq/coq#19985 (template poly has pseudo sort poly)

LPCIC · Jan 17, 2025 · db00ef6 · db00ef6
1 parent d4147f9
commit db00ef6
Showing 1 changed file with 12 additions and 1 deletion.
diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
@@ -2971,7 +2971,7 @@ let poly_cumul_udecl_variance_of_options state options =
 [%%if coq = "8.20"]
 let comInductive_interp_mutual_inductive_constr _ _ _ ~cumulative ~poly ~template ~finite = 
   ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~cumulative ~poly ~template ~finite 
-[%%else]
+[%%elif coq = "9.0"]
 let comInductive_interp_mutual_inductive_constr _ _ _ ~cumulative ~poly ~template ~finite =
   let flags = {
     ComInductive.poly;
@@ -2982,6 +2982,17 @@ let comInductive_interp_mutual_inductive_constr _ _ _ ~cumulative ~poly ~templat
   }
   in
   ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags
+[%%else]
+let comInductive_interp_mutual_inductive_constr _ _ _ ~cumulative ~poly ~template ~finite =
+  let flags = {
+    ComInductive.poly;
+    cumulative;
+    template = Some false;
+    finite;
+    mode = None;
+  }
+  in
+  ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly ()] ~flags
 [%%endif]