Merge pull request #683 from mattam82/typeclasses-default-mode

gares · web-flow · commit d6509831d6b8 · 2024-09-05T12:48:58.000+02:00
Overlay for PR 19473
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`