Adapt to rocq-prover/rocq#19985 (template poly has pseudo sort poly)

SkySkimmer · SkySkimmer · commit d59999a46b5e · 2025-01-23T15:19:37.000+01:00
diff --git 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]
 
 

Original file line number	Diff line number	Diff line change
`@@ -2993,7 +2993,7 @@ let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~fin`
`2993`	`2993`	`}`
`2994`	`2994`	`in`
`2995`	`2995`	`let env_ar = Environ.pop_rel_context (List.length ctx_params) env_ar_params in`
`2996`		`- ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags ~env_ar ~ctx_params`
	`2996`	`+ ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly ()] ~flags ~env_ar ~ctx_params`
`2997`	`2997`	`[%%endif]`
`2998`	`2998`
`2999`	`2999`