honor primitive=off

math-comp · Jun 14, 2024 · b0c98e2 · b0c98e2
1 parent 394ab2c
commit b0c98e2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/HB/factory.elpi b/HB/factory.elpi
@@ -231,8 +231,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
-
-  if (get-option "primitive" tt ; not(Fields = end-record))
+  % TODO cleanup
+  if (get-option "primitive" tt ; (not(get-option "primitive" ff) , not(Fields = end-record)))
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
     (log.coq.env.add-indt RDeclClosed R),