Adapt to coq/coq#18989 (warn when auto lowering inductive to Prop)

LPCIC · Apr 30, 2024 · 6c3e68f · 6c3e68f
1 parent ad4d080
commit 6c3e68f
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
@@ -2893,6 +2893,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
         ~variances
         ~ctx_params:(nuparams @ params)
         ~indnames:[itname]
+        ~arities_explicit:[true]
         ~arities:[arity]
         ~template_syntax:[SyntaxAllowsTemplatePoly]
         ~constructors:[knames, ktypes]