From 401df0b667698bc10952edc31670628cfad9bb41 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 28 Sep 2023 18:28:52 +0200
Subject: [PATCH] Make primitive_class the default

Compilation of MathComp:

* before: 16:34 (1.37 GB)
* after: 14:20 (1.37 GB)
* mathcomp1: 06:16 (0.97 GB) (time x 2.29 (memory x 1.31))

Compilation of Analysis:

* before: 20:59 (1.81 GB)
* after: 12:30 (1.76 GB)
* analysis master: 07:49 (1.55 GB) with HB 1.4 (time x 1.60 (memory x
1.14))
  or 06:32 (1.25 GB) with same HB (time x 1.91 (memory x 1.41))
---
 Changelog.md              | 4 ++++
 HB/common/utils.elpi      | 1 -
 HB/structure.elpi         | 4 +---
 structures.v              | 1 -
 tests/fix_loop.v          | 2 +-
 tests/primitive_records.v | 6 +++---
 6 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index b4dc0c63..76ab679f 100644
--- a/Changelog.md
+++ b/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
diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi
index 8425aa4c..3f94a7ed 100644
--- a/HB/common/utils.elpi
+++ b/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,
diff --git a/HB/structure.elpi b/HB/structure.elpi
index f21d2b9e..2fd1132d 100644
--- a/HB/structure.elpi
+++ b/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
diff --git a/structures.v b/structures.v
index cfe1a247..be0c29fa 100644
--- a/structures.v
+++ b/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.
 *)
 
diff --git a/tests/fix_loop.v b/tests/fix_loop.v
index 176f82fb..96ff0d77 100644
--- a/tests/fix_loop.v
+++ b/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 }.
\ No newline at end of file
+HB.structure Definition S := { A of M A }.
diff --git a/tests/primitive_records.v b/tests/primitive_records.v
index 90ecfb39..232960d2 100644
--- a/tests/primitive_records.v
+++ b/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,7 +33,7 @@ HB.mixin Record HasMul T := {
   mulA: associative mul;
 }.
 
-#[primitive, primitive_class]
+#[primitive]
 HB.structure Definition Mul := { T of HasMul T }.
 
 #[primitive]
@@ -41,6 +41,6 @@ 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 _.