Overlay for PR 19473

mattam82 · mattam82 · commit 615d71c5b343 · 2024-09-02T11:52:49.000+02:00
diff --git 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

Original file line number	Diff line number	Diff line change
`@@ -2962,6 +2962,7 @@ let comInductive_interp_mutual_inductive_constr _ _ _ ~cumulative ~poly ~templat`
`2962`	`2962`	`template = Some false;`
`2963`	`2963`	`auto_prop_lowering = false;`
`2964`	`2964`	`finite;`
	`2965`	`+ mode = None;`
`2965`	`2966`	`}`
`2966`	`2967`	`in`
`2967`	`2968`	`ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags`