Merge pull request #391 from proux01/primitive_class_default

Make primitive_class the default

Author: CohenCyril

Changelog.md

@@ -1,5 +1,9 @@
 # Changelog
 
+## Unreleased
+
+- **Removed** the `#[primitive_class]` attribute, making it the default.
+
 ## [1.6.0] - 2023-09-20
 
 Compatible with

HB/common/utils.elpi

@@ -40,7 +40,6 @@ with-attributes P :-
     att "local" bool,
     att "fail" bool,
     att "doc" string,
-    att "primitive_class" bool,
     att "primitive" bool,
     att "non_forgetful_inheritance" bool,
     att "hnf" bool,

HB/structure.elpi

@@ -466,9 +466,7 @@ declare-class+structure MLwP Sort
     synthesize-fields.body ClassDeclaration,
 
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
-  if (get-option "primitive_class" tt)
-    (@primitive! => log.coq.env.add-indt ClassDeclaration ClassInd)
-    (log.coq.env.add-indt ClassDeclaration ClassInd),
+  (@primitive! => log.coq.env.add-indt ClassDeclaration ClassInd),
 
   coq.env.projections ClassInd Projs,
   % TODO: put this code in a named clause

structures.v

@@ -583,7 +583,6 @@ HB.structure Definition StructureName params :=
   - [#[short(type="shortName")]] produces the abbreviation [shortName] for [Structure.type]
   - [#[short(pack="shortName")]] produces the abbreviation [shortName] for [HB.pack_for Structure.type]
   - [#[primitive]] experimental attribute to make the structure a primitive record,
-  - [#[primitive_class]] experimental attribute to make the class a primitive record,
   - [#[verbose]] for a verbose output.
 *)
 

tests/fix_loop.v

@@ -1,4 +1,4 @@
 From HB Require Import structures.
 
 HB.mixin Record M A := { x: nat }.
-#[primitive_class] HB.structure Definition S := { A of M A }.
+HB.structure Definition S := { A of M A }.

tests/primitive_records.v

@@ -12,7 +12,7 @@ Elpi Query lp:{{
   std.assert! (coq.env.record? Ind tt) "not primitive"
 }}.
 
-#[primitive, primitive_class]
+#[primitive]
 HB.structure Definition A := {T of hasA T}.
 
 Elpi Query lp:{{
@@ -33,14 +33,14 @@ HB.mixin Record HasMul T := {
   mulA: associative mul;
 }.
 
-#[primitive, primitive_class]
+#[primitive]
 HB.structure Definition Mul := { T of HasMul T }.
 
 #[primitive]
 HB.mixin Record HasSq T of Mul T := {
   sq : T -> T;
   pmul : forall x y, sq (mul x y) = mul (sq x) (sq y);
 }.
-#[primitive, primitive_class]
+#[primitive]
 HB.structure Definition Sq := { T of HasSq T & Mul T }.
 Check erefl : Sq.sort _ = Mul.sort _.