diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index da10f6ff0..472cf8222 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -2962,6 +2962,7 @@ let comInductive_interp_mutual_inductive_constr _ _ _ ~cumulative ~poly ~templat template = Some false; auto_prop_lowering = false; finite; + mode = None; } in ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags