Skip to content

Commit 394ab2c

Browse files
committed
always enable primitive mixins
1 parent 873667f commit 394ab2c

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

HB/factory.elpi

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -232,7 +232,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
232232
abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
233233

234234

235-
if (get-option "primitive" tt)
235+
if (get-option "primitive" tt ; not(Fields = end-record))
236236
(@primitive! => log.coq.env.add-indt RDeclClosed R)
237237
(log.coq.env.add-indt RDeclClosed R),
238238

0 commit comments

Comments
 (0)