From 8cdb9d200f1449e25f3e1d1136a907a1b93731e2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 13 Jun 2024 10:17:19 +0200
Subject: [PATCH 1/7] test

---
 _CoqProject.test-suite   |  3 +++
 tests/test_primproj_ty.v | 21 +++++++++++++++++++++
 2 files changed, 24 insertions(+)
 create mode 100644 tests/test_primproj_ty.v

diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
index d60c9bb6c..3d5b4be1a 100644
--- a/_CoqProject.test-suite
+++ b/_CoqProject.test-suite
@@ -95,7 +95,10 @@ tests/unit/close_hole_term.v
 tests/unit/struct.v
 tests/factory_when_notation.v
 
+tests/test_primproj_ty.v
+
 -R tests HB.tests
 -R examples HB.examples
 
+
 -Q . HB
\ No newline at end of file
diff --git a/tests/test_primproj_ty.v b/tests/test_primproj_ty.v
new file mode 100644
index 000000000..7dd225842
--- /dev/null
+++ b/tests/test_primproj_ty.v
@@ -0,0 +1,21 @@
+From Coq Require Import ssreflect ssrfun.
+From HB Require Import structures.
+
+#[primitive]
+HB.mixin Record AddMonoid_of_TYPE S := {
+  zero : S;
+  add : S -> S -> S;
+  addrA : associative add;
+  add0r : left_id zero add;
+  addr0 : right_id zero add;
+}.
+
+HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.
+
+Set Printing All.
+
+Goal let x := @addrA in True.
+match goal with
+| |- let x : forall s : AddMonoid.type, @associative (AddMonoid.sort s) (@add s) := @addrA in True => idtac "OK"
+end.
+Abort.

From ce0707b6a725cda80557be841bf0def2d3757ef0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 13 Jun 2024 11:29:22 +0200
Subject: [PATCH 2/7] kind of works

---
 HB/about.elpi            |  8 +++----
 HB/structure.elpi        | 51 +++++++++++++++++++++++++++++++++-------
 structures.v             |  4 ++--
 tests/test_primproj_ty.v | 20 ++++++++++++++--
 4 files changed, 66 insertions(+), 17 deletions(-)

diff --git a/HB/about.elpi b/HB/about.elpi
index d39dc4585..5f73d7e70 100644
--- a/HB/about.elpi
+++ b/HB/about.elpi
@@ -26,7 +26,7 @@ main-located S (loc-gref (indt I)) :- factory-constructor (indt I) _, !,
 main-located S (loc-gref (const C)) :- factory-constructor (const C) _, !,
   private.main-factory-alias S C.
 
-main-located S (loc-gref (const C)) :- exported-op M _ C, !,
+main-located S (loc-gref (const C)) :- exported-op M _ _ C, !,
   private.main-operation S M C.
 
 main-located S (loc-gref GR) :- factory-alias->gref GR F, not (F = GR), !,
@@ -189,8 +189,8 @@ main-structure S Class Structure MLwP :-
   list-w-params_list MLwP ML,
   std.map-filter ML (m\r\ sigma P O OPS\
     mixin-first-class m Class,
-    std.findall (exported-op m P O) OPS,
-    std.map OPS (c\out\ sigma p\ c = exported-op m p out) r) OPLL,
+    std.findall (exported-op m P _ O) OPS,
+    std.map OPS (c\out\ sigma p\ c = exported-op m p _ out) r) OPLL,
   std.flatten OPLL Operations,
   std.map {std.findall (sub-class Class CS_ CoeS_ NS_)}
     (x\r\ x = sub-class Class r _ _) SubClasses,
@@ -272,7 +272,7 @@ compute-arg-type (w-params.nil ID Ty Rest) F Acc [] ID FN [pr ID PPTy|Xs] :-
   @pi-parameter ID Ty x\ compute-arg-type.fields F {std.length (Rest x)} {std.rev [x|Acc]} Xs FN.
 pred compute-arg-type.fields i:list constant, i:int, i:list term, o:list (pair id coq.pp), o:list id.
 compute-arg-type.fields [] _ _ [] [].
-compute-arg-type.fields [C|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :- exported-op _ C OP, !,
+compute-arg-type.fields [C|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :- exported-op _ C _ OP, !,
   coq.env.typeof (const OP) Ty,
   coq.gref->id (const OP) ID,
   coq.subst-prod Args Ty TyArgs,
diff --git a/HB/structure.elpi b/HB/structure.elpi
index be549496a..9a1192ff4 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -198,19 +198,51 @@ shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }
 % const Po : forall p1 .. pm T m1 .. mn, Extra  (Eg Extra = forall x y, x + y = y + z)
 % const C : forall p1 .. pm s, Extra
 % Po P1 .. PM T M1 .. MN PoArgs -> C P1 .. PM S PoArgs
+pred copy-term i:term, o:term.
+copy-term X Y :- name X, !, X = Y, !. % avoid loading "copy-term x x" at binders
+copy-term (global _ as C) C :- !.
+copy-term (pglobal _ _ as C) C :- !.
+copy-term (sort _ as C) C :- !.
+copy-term (fun N T F) (fun N T1 F1) :- !,
+  copy-term T T1, @pi-decl N T1 x\ copy-term (F x) (F1 x).
+copy-term (let N T B F) (let N T1 B1 F1) :- !,
+  copy-term T T1, copy-term B B1, @pi-def N T1 B1 x\ copy-term (F x) (F1 x).
+copy-term (prod N T F) (prod N T1 F1) :- !,
+  copy-term T T1, (@pi-decl N T1 x\ copy-term (F x) (F1 x)).
+copy-term (app L) (app L1) :- !, std.map L copy-term L1.
+copy-term (fix N Rno Ty F) (fix N Rno Ty1 F1) :- !,
+  copy-term Ty Ty1, @pi-decl N Ty1 x\ copy-term (F x) (F1 x).
+copy-term (match T Rty B) (match T1 Rty1 B1) :- !,
+  copy-term T T1, copy-term Rty Rty1, std.map B copy-term B1.
+copy-term (primitive _ as C) C :- !.
+copy-term (uvar M L as X) W :- var X, !, std.map L copy-term L1, coq.mk-app-uvar M L1 W.
+% when used in CHR rules
+copy-term (uvar X L) (uvar X L1) :- std.map L copy-term L1.
+
+
 pred clean-op-ty i:list prop, i:term, i:term, o:term.
-clean-op-ty [] _ T1 T2 :- copy T1 T2.
-clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
+clean-op-ty [] _ T1 T2 :- copy-term T1 T2.
+clean-op-ty [exported-op _ Po PrimPop C|Ops] S T1 T2 :-
   gref-deps (const Po) MLwP,
   w-params.nparams MLwP NParams,
   std.length {list-w-params_list MLwP} NMixins,
 
   (pi L L1 L2 Params Rest PoArgs\
-    copy (app [global (const Po)| L]) (app [global (const C) | L2]) :-
+    copy-term (app [global (const Po)| L]) (app [global (const C) | L2]) :-
       std.split-at NParams L Params [_|Rest],
       std.drop NMixins Rest PoArgs,
       std.append Params [S|PoArgs] L1,
-      std.map L1 copy L2) =>
+      std.map L1 copy-term L2) =>
+
+  (pi P N L1 L2 L3 TheMixin Params Ty\
+     % even if NMixins > 1, they are parameters of the primitive projection so
+     % they are not present
+     copy-term (app [primitive (proj P N), TheMixin|L1]) (app [global (const C) | L3]) :- PrimPop = some (pr P N), !,
+       coq.mk-n-holes NParams Params,
+       std.append Params [S|L1] L2,
+       std.map L2 copy-term L3,
+       std.assert-ok! (coq.typecheck (app [global (const C) | L3]) Ty) "clean-op-ty") =>
+
   clean-op-ty Ops S T1 T2.
 
 pred operation-body-and-ty i:list prop, i:constant, i:structure, i:term, i:term,
@@ -237,9 +269,9 @@ operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ Par
 % same operation out of the package structure (out of the class field of the
 % structure). We also provide all the other mixin dependencies (other misins)
 % of the package structure.
-pred export-1-operation i:mixinname, i:structure, i:term, i:term, i:one-w-params mixinname, i:option constant, i:list prop, o:list prop.
-export-1-operation _ _ _ _ _ none EX EX :- !. % not a projection, no operation
-export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std.do! [
+pred export-1-operation i:mixinname, i:structure, i:term, i:term, i:one-w-params mixinname, i:option constant, i:option (pair projection int), i:list prop, o:list prop.
+export-1-operation _ _ _ _ _ none _ EX EX :- !. % not a projection, no operation
+export-1-operation M Struct Psort Pclass MwP (some Poperation) PrimPop EXI EXO :- !, std.do! [
   coq.gref->id (const Poperation) Name,
 
   w-params.then MwP mk-fun-prod ignore (operation-body-and-ty EXI Poperation Struct Psort Pclass) (pr Body BodyTy),
@@ -253,7 +285,7 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std
   std.map INI (_\r\ r = maximal) Implicits,
   @global! => log.coq.arguments.set-implicit (const C) [Implicits],
 
-  EXO = [exported-op M Poperation C|EXI]
+  EXO = [exported-op M Poperation PrimPop C|EXI]
 ].
 
 % Given a list of mixins, it exports all operations in there
@@ -261,7 +293,8 @@ pred export-operations.aux i:structure, i:term, i:term, i:one-w-params mixinname
 export-operations.aux Struct ProjSort ProjClass MwP EX1 EX2 :- !, std.do! [
   w-params_1 MwP (indt M),
   coq.env.projections M Poperations,
-  std.fold Poperations EX1 (export-1-operation (indt M) Struct ProjSort ProjClass MwP) EX2,
+  coq.env.primitive-projections M PrimPoperations,
+  std.fold2 Poperations PrimPoperations EX1 (export-1-operation (indt M) Struct ProjSort ProjClass MwP) EX2,
 ].
 
 pred mixin-not-already-declared i:one-w-params mixinname.
diff --git a/structures.v b/structures.v
index 027c14427..748b3c986 100644
--- a/structures.v
+++ b/structures.v
@@ -171,8 +171,8 @@ pred mixin-mem i:term, o:gref.
 % that contains the mixin M
 pred mixin-first-class o:mixinname, o:classname.
 
-% memory of exported operations (TODO: document fiels)
-pred exported-op o:mixinname, o:constant, o:constant.
+% memory of exported operations [exported-op Mixin MixinProj PrimitiveMixinProj StructureProj]
+pred exported-op o:mixinname, o:constant, o:option (pair projection int), o:constant.
 
 % memory of factory sort coercion
 pred factory-sort o:coercion.
diff --git a/tests/test_primproj_ty.v b/tests/test_primproj_ty.v
index 7dd225842..d0eb72e18 100644
--- a/tests/test_primproj_ty.v
+++ b/tests/test_primproj_ty.v
@@ -12,10 +12,26 @@ HB.mixin Record AddMonoid_of_TYPE S := {
 
 HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.
 
-Set Printing All.
-
 Goal let x := @addrA in True.
 match goal with
 | |- let x : forall s : AddMonoid.type, @associative (AddMonoid.sort s) (@add s) := @addrA in True => idtac "OK"
 end.
 Abort.
+
+#[primitive]
+HB.mixin Record Scale_of_AddMonoid (P : Type) S of AddMonoid_of_TYPE S := {
+  scale : P -> S -> S;
+  scaleBad : forall p (x y : S), (* HUMMM, if I don't put S here, it infers the eta expansion of S *)
+    scale p (add x y) = add (scale p x) (scale p y);
+}.
+
+About Scale_of_AddMonoid.scale.
+
+HB.structure Definition ScaleMonoid P := { A of Scale_of_AddMonoid P A }.
+
+Goal let a := @scaleBad in True.
+match goal with
+| |- let a : forall P (s : ScaleMonoid.type P), forall p : P, forall x y : ScaleMonoid.sort P s, scale p (add x y) = add (scale p x) (scale p y) := @scaleBad in True => idtac "OK"
+end.
+Abort.
+

From 873667fe9b56677228fd8a878ee0b68bd4c499b4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 13 Jun 2024 13:57:17 +0200
Subject: [PATCH 3/7] hack for coq.term->gref

---
 HB/common/stdpp.elpi | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index 5a5b85e10..b098eff3b 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -260,6 +260,16 @@ term->cs-pattern (sort U) (cs-sort U).
 term->cs-pattern T (cs-gref GR) :- coq.term->gref T GR.
 term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key".
 
+%hack/missing API
+:before "stop:begin"
+coq.term->gref (app [primitive (proj N J),T|_]) GR :- !, std.do! [
+  coq.typecheck T Ty ok,
+  coq.term->gref Ty (indt I),
+  coq.env.projections I Ps,
+  coq.env.primitive-projections I PPs,
+  std.map2-filter Ps PPs (x\y\gr\sigma c\x = some c, y = some (pr N J), gr = const c) [GR],
+].
+
 pred cs-pattern->name i:cs-pattern, o:string.
 cs-pattern->name cs-prod "prod".
 cs-pattern->name (cs-sort _) "sort".

From 394ab2c19b62530b01397baa76f726211164c72b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 13 Jun 2024 13:57:28 +0200
Subject: [PATCH 4/7] always enable primitive mixins

---
 HB/factory.elpi | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index 8ff726654..54a3afd95 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -232,7 +232,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
 
-  if (get-option "primitive" tt)
+  if (get-option "primitive" tt ; not(Fields = end-record))
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
     (log.coq.env.add-indt RDeclClosed R),
 

From b0c98e2fcb6d432d1d9ff823b2d4c82636a382a2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 14 Jun 2024 14:20:34 +0200
Subject: [PATCH 5/7] honor primitive=off

---
 HB/factory.elpi | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index 54a3afd95..dd829a5ee 100644
--- 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),
 

From b4d1844281a3dbbd8f20ee157e819036fbffda6d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Tue, 18 Jun 2024 16:12:57 +0200
Subject: [PATCH 6/7] use primproj for class->mixin builders

---
 HB/about.elpi            |  2 +-
 HB/builders.elpi         |  2 +-
 HB/common/database.elpi  | 16 +++++++++++-----
 HB/common/stdpp.elpi     |  5 +++++
 HB/common/synthesis.elpi |  6 ++++--
 HB/factory.elpi          |  2 +-
 HB/instance.elpi         |  2 +-
 HB/status.elpi           |  6 +++++-
 HB/structure.elpi        | 13 +++++++++----
 structures.v             | 16 +++++++++++-----
 10 files changed, 49 insertions(+), 21 deletions(-)

diff --git a/HB/about.elpi b/HB/about.elpi
index 5f73d7e70..516b77507 100644
--- a/HB/about.elpi
+++ b/HB/about.elpi
@@ -41,7 +41,7 @@ main-located S (loc-abbreviation A) :-
   coq.safe-dest-app T (global GR) _, !,
   main-located S (loc-gref GR).
 
-main-located S (loc-gref GR) :- from Factory Mixin GR, !,
+main-located S (loc-gref GR) :- from Factory Mixin (gref GR), !,
   private.main-builder S Factory Mixin.
 
 main-located S (loc-gref GR) :-
diff --git a/HB/builders.elpi b/HB/builders.elpi
index 37493db36..ec3f31226 100644
--- a/HB/builders.elpi
+++ b/HB/builders.elpi
@@ -79,7 +79,7 @@ pred declare-1-builder i:builder, i:list prop, o:list prop.
 declare-1-builder (builder _ SrcFactory TgtMixin _) FromClauses FromClauses :- FromClauses => from SrcFactory TgtMixin _, !,
   if-verbose (coq.say {header} "skipping duplicate builder from"
     {nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}).
-declare-1-builder (builder _ SrcFactory TgtMixin B) FromClauses [from SrcFactory TgtMixin B|FromClauses] :-
+declare-1-builder (builder _ SrcFactory TgtMixin B) FromClauses [from SrcFactory TgtMixin (gref B)|FromClauses] :-
   if-verbose (coq.say {header} "declare builder from"
     {nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}).
 
diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index d583b4c37..b214e0727 100644
--- a/HB/common/database.elpi
+++ b/HB/common/database.elpi
@@ -11,8 +11,8 @@ from_factory (from X _ _) X.
 pred from_mixin i:prop, o:mixinname.
 from_mixin (from _ X _) X.
 
-pred from_builder i:prop, o:term.
-from_builder (from _ _ X) (global X).
+pred from_builder i:prop, o:gref-or-primitive.
+from_builder (from _ _ X) X.
 
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
@@ -104,12 +104,18 @@ factory-provides.base Factory Params T _RMLwP MLwP :- std.do! [
   std.map2 BL ML (factory-provides.one Params T) MLwP,
 ].
 
-pred factory-provides.one i:list term, i:term, i:term, i:mixinname, o:w-args mixinname.
-factory-provides.one Params T B M (triple M PL T) :- std.do! [
-  std.assert-ok! (coq.typecheck B Ty) "Builder illtyped",
+pred factory-provides.one i:list term, i:term, i:gref-or-primitive, i:mixinname, o:w-args mixinname.
+factory-provides.one Params T (gref B) M (triple M PL T) :- std.do! [
+  coq.env.typeof B Ty,
   subst-prod [T] {subst-prod Params Ty} TyParams,
   std.assert! (extract-conclusion-params T TyParams PL) "The conclusion of a builder is a mixin whose parameters depend on other mixins",
 ].
+factory-provides.one Params T (primitive (pr P N)) M (triple M PL T) :- std.do! [
+  coq.mk-app {coq.mk-app (global M) Params} [T] TyM, % fine since M is the class hence no extra arg needed
+  std.assert-ok! (d\@pi-decl `m` TyM m\coq.typecheck (app[primitive(proj P N),m]) (TyParams m) d) "Builder illtyped",
+  @pi-decl `m` TyM m\
+    std.assert! (extract-conclusion-params T (TyParams m) PL) "The conclusion of a primitive projection is a mixin whose parameters depend on other mixins"
+].
 
 pred extract-conclusion-params i:term, i:term, o:list term.
 extract-conclusion-params TheType (prod _ S T) R :- !,
diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index b098eff3b..341bcf49f 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -270,6 +270,11 @@ coq.term->gref (app [primitive (proj N J),T|_]) GR :- !, std.do! [
   std.map2-filter Ps PPs (x\y\gr\sigma c\x = some c, y = some (pr N J), gr = const c) [GR],
 ].
 
+%hack/ fixup API
+:before "subst-fun:fail"
+coq.subst-fun L (primitive (proj _ _) as F) (app[F|L]).
+
+
 pred cs-pattern->name i:cs-pattern, o:string.
 cs-pattern->name cs-prod "prod".
 cs-pattern->name (cs-sort _) "sort".
diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi
index c596fc5c4..39359c93c 100644
--- a/HB/common/synthesis.elpi
+++ b/HB/common/synthesis.elpi
@@ -223,13 +223,15 @@ mixin-for_mixin-builder (mixin-for _ _ B) B.
 % and fills in all the mixins required by the builder using mixin-src, obtaining
 % a function (MF = Builder Params TheType InferredStuff : Src -> Tgt)
 pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term.
-builder->term Ps T Src Tgt B :- !, std.do! [
-  from Src Tgt FGR,
+builder->term Ps T Src Tgt B :- from Src Tgt (gref FGR), !, std.do! [
   F = global FGR,
   gref-deps Src MLwP,
   list-w-params_list MLwP ML,
   infer-all-these-mixin-args Ps T ML F B,
 ].
+builder->term _ _ Src Tgt (primitive (proj P N)) :-
+  % no deps, Src is a class
+  from Src Tgt (primitive (pr P N)).
 
 % [instantiate-all-these-mixin-args T F M_i TFX] where mixin-for T M_i X_i states that
 % if    F  ~  fun xs (m_0 : M_0 T) .. (m_n : M_n T ..) ys
diff --git a/HB/factory.elpi b/HB/factory.elpi
index dd829a5ee..b5a272b70 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -165,7 +165,7 @@ cdecl->w-mixins.mixins (context-item ID _ TySkel none Rest) Out :- !,
 
 % The identity builder
 pred declare-id-builder i:factoryname, o:prop.
-declare-id-builder GR (from GR GR (const C)) :- std.do! [
+declare-id-builder GR (from GR GR (gref (const C))) :- std.do! [
   gref-deps GR GRD,
   synthesis.mixins-w-params.fun GRD (declare-id-builder.aux GR) IDBodySkel,
   std.assert-ok! (coq.elaborate-skeleton IDBodySkel IDType IDBody) "identity builder illtyped",
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 2eec1d08b..f4b81c152 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -406,7 +406,7 @@ optimize-class-body _ _ (app L) (app L) [].
 pred declare-mixin-name i:term, o:term, o:list prop.
 declare-mixin-name (global _ as T) T [].
 declare-mixin-name T (global GR) [] :- mixin-mem T GR.
-declare-mixin-name T T [] :- coq.safe-dest-app T (global GR) _, not (from _ _ GR), not (get-option "hnf" tt).
+declare-mixin-name T T [] :- coq.safe-dest-app T (global GR) _, not (from _ _ (gref GR)), not (get-option "hnf" tt).
 declare-mixin-name T (global (const C)) [mixin-mem T (const C)] :- std.do! [
   Name is "HB_unnamed_mixin_" ^ {std.any->string {new_int}},
   if-verbose (coq.say {header} "Giving name" Name "to mixin instance" {coq.term->string T}),
diff --git a/HB/status.elpi b/HB/status.elpi
index e6bf3684e..5699194f6 100644
--- a/HB/status.elpi
+++ b/HB/status.elpi
@@ -43,10 +43,14 @@ print-hierarchy :- std.do! [
 namespace private {
 
 pred pp-from i:prop.
-pp-from (from F M T) :-
+pp-from (from F M (gref T)) :-
   coq.say "From" {coq.term->string (global F)} "to" {coq.term->string (global M)},
   coq.say "  " {coq.term->string (global T)},
   coq.say "".
+pp-from (from F M (primitive (pr P N))) :-
+  coq.say "From" {coq.term->string (global F)} "to" {coq.term->string (global M)},
+  coq.say "  " P " (" N "th field)",
+  coq.say "".
 
 pred pp-list-w-params i:mixins, i:term.
 pred pp-list-w-params.list-triple i:list (w-args mixinname), i:term.
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 9a1192ff4..ddbf1fb3e 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -309,6 +309,11 @@ export-operations Structure ProjSort ProjClass MLwP EX1 EX2 MLToExport :- std.do
   std.map LMwPToExport w-params_1 MLToExport,
 ].
 
+pred mk-app-builder i:list term, i:term, i:gref-or-primitive, o:term.
+mk-app-builder Params TheType (gref B) T :-
+  coq.mk-app {coq.env.global B} {std.append Params [TheType]} T.
+mk-app-builder _ _ (primitive (pr P N)) (primitive(proj P N)).
+
 pred mk-coe-class-body
   i:factoryname, % From class
   i:factoryname, % To class
@@ -321,14 +326,14 @@ mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [
 
   list-w-params_list TMLwP TML,
   std.map TML (from FC) Builders,
-  std.map Builders (x\r\mk-app (global x) Params r) BuildersP,
+  std.map Builders (mk-app-builder Params T) BuildersP,
 
   factory-nparams TC TCNP,
   mk-app (global {get-constructor TC})
     {coq.mk-n-holes TCNP} KCHoles,
 
   (pi c\ sigma Mixes\
-    std.map BuildersP (builder\r\ r = app[builder, T, c]) Mixes,
+    std.map BuildersP (builder\r\ r = app[builder, c]) Mixes,
     mk-app KCHoles [T | Mixes] (ClassCoercion c)),
 
   CoeBody = {{ fun (c : lp:Class) => lp:(ClassCoercion c) }}
@@ -497,12 +502,12 @@ declare-class+structure MLwP Sort
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
   (@primitive! => log.coq.env.add-indt ClassDeclaration ClassInd),
 
-  coq.env.projections ClassInd Projs,
+  coq.env.primitive-projections ClassInd Projs,
   % TODO: put this code in a named clause
   w-params.nparams MLwP NParams,
   std.map2 {list-w-params_list MLwP} Projs (m\ p\ r\ sigma P\
     std.assert! (p = some P) "BUG: we build a class with an anonymous field",
-    r = from (indt ClassInd) m (const P)) Factories,
+    r = from (indt ClassInd) m (primitive P)) Factories,
   AllFactories = [factory-nparams (indt ClassInd) NParams | Factories],
 
   if-verbose (coq.say {header} "declare type record"),
diff --git a/structures.v b/structures.v
index 748b3c986..9c77a4ad0 100644
--- a/structures.v
+++ b/structures.v
@@ -109,13 +109,19 @@ pred class-def o:class.
 
 %%%%% Builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-% [from FN MN F] invariant:
-% "F : forall p1 .. pn T LMN, FN p1 .. pn T LMN1 -> MN c1 .. cm T LMN2" where
-%  - LMN1 and LMN2 are sub lists of LMN
-%  - c1 .. cm are terms built using p1 .. pn and T
+% [from FN MN B] invariant:
+% - B = gref F
+%   "F : forall p1 .. pn T LMN, FN p1 .. pn T LMN1 -> MN c1 .. cm T LMN2" where
+%    - LMN1 and LMN2 are sub lists of LMN
+%    - c1 .. cm are terms built using p1 .. pn and T
+% - B = primitive (pr P N)
+%    - as above but no parameters
 % - [factory-requires FN LMN]
 % [from _ M _] tests whether M is a declared mixin.
-pred from o:factoryname, o:mixinname, o:gref.
+kind gref-or-primitive type.
+type gref gref -> gref-or-primitive.
+type primitive pair projection int -> gref-or-primitive.
+pred from o:factoryname, o:mixinname, o:gref-or-primitive.
 
 %%%%% Abbreviations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 

From 5b4a090fc1773a2b40121a9166bfbc34c8a441c4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Wed, 19 Jun 2024 10:24:36 +0200
Subject: [PATCH 7/7] Update config.nix

---
 .nix/config.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.nix/config.nix b/.nix/config.nix
index 67403a3fb..1cefde318 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -22,7 +22,7 @@
     };
   in {
     "coq-master".coqPackages = mcHBcommon // {
-      coq.override.version = "master";
+      coq.override.version = "proux01:ssrmatching_primitive_proj";
       coq-elpi.override.version = "coq-master";
       bignums.override.version = "master";
       paramcoq.override.version = "master";