From e69376e09ebc3fbfe7c3588252f0ac47b3d847f1 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Thu, 26 Jun 2025 16:28:23 +0200
Subject: [PATCH 01/28] pack done, about wip

---
 HB/about.elpi |  2 +-
 HB/pack.elpi  | 14 +++++++-------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/HB/about.elpi b/HB/about.elpi
index 0c2c2806d..71af15a8c 100644
--- a/HB/about.elpi
+++ b/HB/about.elpi
@@ -38,7 +38,7 @@ main-located S (loc-abbreviation A) :- phant-abbrev GR PhB A, factory-constructo
 main-located S (loc-abbreviation A) :-
   coq.notation.abbreviation-body A NArgs _,
   coq.notation.abbreviation A {coq.mk-n-holes NArgs} T,
-  coq.safe-dest-app T (global GR) _, !,
+  coq.safe-dest-app T THead _, coq.env.global GR THead, !,
   main-located S (loc-gref GR).
 
 main-located S (loc-gref GR) :- from Factory Mixin GR, !,
diff --git a/HB/pack.elpi b/HB/pack.elpi
index 3bd0d2cc0..3e265c308 100644
--- a/HB/pack.elpi
+++ b/HB/pack.elpi
@@ -23,8 +23,8 @@ main Ty Args Instance :- std.do! [
 
   if (var T) (coq.error "HB.pack: you must pass a type or at least one factory") true,
 
-  if2 (T = app[global (const SortProj)|ProjParams], structure-key SortProj ClassProj _)
-        (AllFactories = [app[global (const ClassProj)|ProjParams] | Factories], Tkey = T) % already existing class on T
+    if2 (T = app[SortProjHead|ProjParams], coq.env.global (const SortProj) SortProjHead, structure-key SortProj ClassProj _)
+        (AllFactories = [app[ClassProjHead|ProjParams] | Factories], coq.env.global (const ClassProj) ClassProjHead, Tkey = T) % already existing class on T
       (def T _ _ Tkey) % we unfold letins if we can, they may hide constants with CS instances
         (AllFactories = Factories)
       (AllFactories = Factories, Tkey = T), % it's a factory, won't add anything
@@ -47,12 +47,12 @@ synth-instance.aux Params KC KS T Tkey [] MLCano Instance :-
 	MLCano => std.do! [
     std.assert-ok! (synthesis.infer-all-args-let Params Tkey KC ClassInstance) "HB.pack: cannot infer the instance",
     std.append Params [T, ClassInstance] InstanceArgs,
-      Instance = app[global KS | InstanceArgs]
+      Instance = app[Head | InstanceArgs], coq.env.global KS Head
 ].
 
 pred synth-instance i:list term, i:gref, i:gref, i:term, i:term, i:list term, o:term.
 synth-instance Params KC KS T Tkey Factories Instance :-
-	if (coq.safe-dest-app Tkey (global _) _) (synthesis.local-canonical-mixins-of Tkey MLCano) (MLCano = []),
+	if (coq.safe-dest-app Tkey TkeyHead _, coq.env.global _ TkeyHead) (synthesis.local-canonical-mixins-of Tkey MLCano) (MLCano = []),
 	synth-instance.aux Params KC KS T Tkey Factories MLCano Instance.
 
 pred elab-factories i:list argument, i:term, o:list term.
@@ -61,11 +61,11 @@ elab-factories [trm FactorySkel|More] T [Factory|Factories] :-
   std.assert-ok! (coq.elaborate-skeleton FactorySkel FTy MaybeFactory) "HB.pack: illtyped factory",
   if2 (factory? {unwind {whd FTy []}} (triple _ _ T1)) % a factory
         (Factory = MaybeFactory)
-      (coq.safe-dest-app {unwind {whd FTy []}}  (global GR) _, structure-key SortP ClassP GR) % a structure instance
+      (coq.safe-dest-app {unwind {whd FTy []}}  TyHead _, coq.env.global GR TyHead, structure-key SortP ClassP GR) % a structure instance
         (coq.mk-n-holes {structure-nparams GR} Params,
          std.append Params [MaybeFactory] ParamsF,
-         coq.mk-app (global (const SortP)) ParamsF T1,
-         coq.mk-app (global (const ClassP)) ParamsF Factory)
+         coq.mk-app {coq.env.global (const SortP)} ParamsF T1,
+         coq.mk-app {coq.env.global (const ClassP)} ParamsF Factory)
       (coq.error "HB: argument" {coq.term->string MaybeFactory} "is not a factory, it has type:" {coq.term->string FTy}),
   std.assert-ok! (coq.unify-eq T T1) "HB.pack: factory for the wrong type",
   elab-factories More T Factories.

From 47bba2da0a490deba3753e7a9eed5765802d93a4 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Thu, 26 Jun 2025 16:43:33 +0200
Subject: [PATCH 02/28] wip

---
 HB/about.elpi        | 8 ++++----
 HB/common/utils.elpi | 5 +++++
 HB/pack.elpi         | 4 ++--
 3 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/HB/about.elpi b/HB/about.elpi
index 71af15a8c..9e5ecde58 100644
--- a/HB/about.elpi
+++ b/HB/about.elpi
@@ -38,7 +38,7 @@ main-located S (loc-abbreviation A) :- phant-abbrev GR PhB A, factory-constructo
 main-located S (loc-abbreviation A) :-
   coq.notation.abbreviation-body A NArgs _,
   coq.notation.abbreviation A {coq.mk-n-holes NArgs} T,
-  coq.safe-dest-app T THead _, coq.env.global GR THead, !,
+  coq.safe-dest-global-app T GR _, !,
   main-located S (loc-gref GR).
 
 main-located S (loc-gref GR) :- from Factory Mixin GR, !,
@@ -143,7 +143,7 @@ main-canonical-projection S Proj CanonicalProjectionValues :-
 
 pred pp-canonical-value i:cs-instance, o:coq.pp.
 pp-canonical-value (cs-instance _Proj (cs-gref GR) _Sol) Pp :-
-  coq.term->pp (global GR) V,
+  coq.term->pp {coq.env.global GR} V,
   Pp = box (hov 2) [ V , spc, {pp-loc-of GR} ].
 
 pred main-coercion i:string, i:list coercion.
@@ -151,11 +151,11 @@ main-coercion S [coercion GR _ Src Tgt|_] :-
   % format
   if (class-def (class _ Src _) ; class-def (class Src _ _))
      (Source = str {gref->modname_short Src "."})
-     (coq.term->pp (global Src) Source),
+     (coq.term->pp {coq.env.global Src} Source),
   if2 (Tgt = grefclass TGR)
         (if (class-def (class _ TGR _) ; class-def (class TGR _ _))
           (Target = str {gref->modname_short TGR "."})
-          (coq.term->pp (global TGR) Target))
+          (coq.term->pp {coq.env.global TGR} Target))
       (Tgt = sortclass)
         (Target = str "Sortclass")
       (Target = str "Funclass"),
diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi
index ae4216b66..93c8d2039 100644
--- a/HB/common/utils.elpi
+++ b/HB/common/utils.elpi
@@ -98,6 +98,11 @@ gref->modname_short1 MP S _ S :- string->modpath S MP.
 gref->modname_short1 MP S [X|L] S' :-
   gref->modname_short1 MP {std.string.concat "." [X,S]} L S'.
 
+pred coq.safe-dest-global-app i:term, o:gref, o:list term.
+coq.safe-dest-global-app Tm GR Args :- !, std.do![
+    coq.safe-dest-app Tm Head Args, coq.env.global GR Head
+  ].
+
 % Print shortest qualified identifier of the module containing a gref
 % Sep is used as separator
 pred gref->modname_short i:gref, i:string, o:string.
diff --git a/HB/pack.elpi b/HB/pack.elpi
index 3e265c308..c18645c35 100644
--- a/HB/pack.elpi
+++ b/HB/pack.elpi
@@ -7,7 +7,7 @@ namespace pack {
 pred main i:term, i:list argument, o:term.
 main Ty Args Instance :- std.do! [
   std.assert! (not(var Ty)) "HB.pack: the structure to pack cannot be unknown, use HB.pack_for",
-  std.assert! (coq.safe-dest-app {unwind {whd Ty []}} (global Structure) Params) "HB.pack: not a structure",
+  std.assert! (coq.safe-dest-global-app {unwind {whd Ty []}} Structure Params) "HB.pack: not a structure",
   std.assert! (class-def (class Class Structure _)) "HB.pack: not a structure",
   std.assert! (Args = [trm TSkel|FactoriesSkel]) "HB.pack: not enough arguments",
 
@@ -52,7 +52,7 @@ synth-instance.aux Params KC KS T Tkey [] MLCano Instance :-
 
 pred synth-instance i:list term, i:gref, i:gref, i:term, i:term, i:list term, o:term.
 synth-instance Params KC KS T Tkey Factories Instance :-
-	if (coq.safe-dest-app Tkey TkeyHead _, coq.env.global _ TkeyHead) (synthesis.local-canonical-mixins-of Tkey MLCano) (MLCano = []),
+	if (coq.safe-dest-global-app Tkey _ _) (synthesis.local-canonical-mixins-of Tkey MLCano) (MLCano = []),
 	synth-instance.aux Params KC KS T Tkey Factories MLCano Instance.
 
 pred elab-factories i:list argument, i:term, o:list term.

From ab105f133a11d67c6bd42b1c72826387fdb3b63b Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Thu, 26 Jun 2025 16:48:44 +0200
Subject: [PATCH 03/28] done about

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

diff --git a/HB/about.elpi b/HB/about.elpi
index 9e5ecde58..87d36fbb0 100644
--- a/HB/about.elpi
+++ b/HB/about.elpi
@@ -291,7 +291,7 @@ compute-arg-type.fields [OP|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :-
   (@pplevel! 200 => coq.term->pp TyArgsDepsRecord PPTy),
   @pi-parameter ID TyArgsDepsRecord op\
   (pi L L1 X\
-    copy (app[global(const OP)|L]) X :- std.drop ToDrop L L1, coq.mk-app op L1 X) =>
+    copy (app[{coq.env.global (const OP)}|L]) X :- std.drop ToDrop L L1, coq.mk-app op L1 X) =>
     compute-arg-type.fields Cs NDeps Args Xs FN.
 
 pred main-factory i:string, i:inductive.

From 17e5e38df733d76951384a20dff9c1d3f84c4c3c Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Thu, 26 Jun 2025 16:50:16 +0200
Subject: [PATCH 04/28] done context

---
 HB/context.elpi | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/HB/context.elpi b/HB/context.elpi
index 4b04e5f0b..3dc2d9b95 100644
--- a/HB/context.elpi
+++ b/HB/context.elpi
@@ -16,14 +16,14 @@ declare.params-key MLwP Params TheKey Out :- !, std.do! [
   if-verbose (coq.say {header} "declaring parameters and key as section variables"),
   declare.params MLwP Params KId KTy F,
   log.coq.env.add-section-variable-noimplicits KId KTy C,
-  TheKey = global (const C),
+  coq.env.global (const C) TheKey,
   Out = F TheKey
 ].
 
 pred declare.params i:w-params A, o:list (triple id term term), o:id, o:term, o:(term -> A).
 declare.params (w-params.cons PId PTy F) [triple PId P PTy|Params] KId KTy Out :- !, std.do! [
   log.coq.env.add-section-variable-noimplicits PId PTy C,
-  P = global (const C),
+  coq.env.global (const C) P,
   declare.params (F P) Params KId KTy Out
 ].
 declare.params (w-params.nil KId KTy F) [] KId KTy F :- !.
@@ -71,7 +71,8 @@ postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|M
   log.coq.env.add-section-variable-noimplicits Name Ty C,
   factory? Ty NewMwP,
 
-  MC = mixin-src T M (global (const C)),
+  coq.env.global (const C) Tm,
+  MC = mixin-src T M Tm,
   MC => get-option "local" tt =>
     instance.declare-all TheType {findall-classes-for [M]} NewCSL,
   std.map NewCSL snd NewCL,

From e553d432f81991118df1df7676bbcfde40fb2058 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Thu, 26 Jun 2025 17:10:46 +0200
Subject: [PATCH 05/28] done status and factory

---
 HB/factory.elpi | 13 ++++++++-----
 HB/status.elpi  |  8 ++++----
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index ef00f61ac..c1ecc639f 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -16,7 +16,8 @@ type by-phantabbrev abbreviation -> factory-abbrev.
 pred declare-abbrev i:id, i:factory-abbrev, o:abbreviation.
 declare-abbrev Name (by-classname GR) Abbrev :-
   % looks fishy (the parameters are not taken into account)
-  @global! => log.coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt Abbrev.
+  coq.env.global GR Tm,
+  @global! => log.coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[Tm, t]) tt Abbrev.
 declare-abbrev Name (by-phantabbrev Abbr) Abbrev :- std.do! [
   coq.notation.abbreviation-body Abbr Nargs AbbrTrm,
   @global! => log.coq.notation.add-abbreviation Name Nargs AbbrTrm tt Abbrev,
@@ -316,13 +317,15 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr Ty1 _) (pr Ty1Closed _) Section,
   log.coq.env.add-const-noimplicits "axioms_" Ty1Closed _ @transparent! C,
 
-  std.assert! (safe-dest-app Ty1 (global PhF) _Args) "Argument must be a factory",
+  std.assert! (coq.safe-dest-global-app Ty1 PhF _Args) "Argument must be a factory",
   std.assert-ok! (factory-alias->gref PhF F) "HB",
   std.assert! (factory-constructor F FK) "BUG: Factory constructor missing",
 
   MixinSrcClauses => synthesis.infer-all-gref-deps TheParams TheType FK MFK,
   std.assert-ok! (coq.typecheck MFK MFKTy) "BUG: typecking of former factory constructor failed",
-  (pi Args\ copy (app[global F|Args]) (app[global (const C)|Section])) => copy MFKTy MFKTyC,
+  coq.env.global F FHead,
+  coq.env.global (const C) CHead,
+  (pi Args\ copy (app[FHead|Args]) (app[CHead|Section])) => copy MFKTy MFKTyC,
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr MFK MFKTyC) (pr MFKClosed MFKTyCClosed) _,
   log.coq.env.add-const-noimplicits "Axioms_" MFKClosed MFKTyCClosed @transparent! CK,
@@ -393,7 +396,7 @@ abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance
   % compute section variables to be used for discharging
   std.map MixinSrcClauses mixin-src_src Mixins,
   std.append TheParams [TheType|{std.rev Mixins}] Section,
-  std.map Section (x\r\ x = global (const r)) SectionVars,
+  std.map Section (x\r\ coq.env.global (const r) x) SectionVars,
   % We discharge by hand the record declaration so that we can be sure all
   % parameters and mixins are abstracted (even if unused).
   coq.copy-clauses-for-unfold SectionCanonicalInstance CopyUnfold,
@@ -415,4 +418,4 @@ mk-factory-sort.term GR P T (fun `_` Ty _\ T) :- synthesis.infer-all-gref-deps P
 
 
 
-}}
\ No newline at end of file
+}}
diff --git a/HB/status.elpi b/HB/status.elpi
index e6bf3684e..1913072b9 100644
--- a/HB/status.elpi
+++ b/HB/status.elpi
@@ -44,8 +44,8 @@ namespace private {
 
 pred pp-from i:prop.
 pp-from (from F M T) :-
-  coq.say "From" {coq.term->string (global F)} "to" {coq.term->string (global M)},
-  coq.say "  " {coq.term->string (global T)},
+  coq.say "From" {coq.term->string {coq.env.global F}} "to" {coq.term->string {coq.env.global M}},
+  coq.say "  " {coq.term->string {coq.env.global T}},
   coq.say "".
 
 pred pp-list-w-params i:mixins, i:term.
@@ -59,11 +59,11 @@ pp-list-w-params.list-triple L S :-
   coq.say {coq.term->string S} ":=",
   std.forall L pp-list-w-params.triple.
 pp-list-w-params.triple (triple M Params T) :-
-  coq.say "  " {coq.term->string (app [global M|{std.append Params [T]}])}.
+  coq.say "  " {coq.term->string (app [{coq.env.global M}|{std.append Params [T]}])}.
 
 pred pp-class i:prop.
 pp-class (class-def (class _ S MLwP)) :-
-  pp-list-w-params MLwP (global S).
+  pp-list-w-params MLwP {coq.env.global S}.
 
 pred pp-mixin-src i:prop.
 pp-mixin-src (mixin-src T M C) :-

From e8a3faf71f6110f7e6cbde15f7b770656b8a5f00 Mon Sep 17 00:00:00 2001
From: qvermande <quentin.vermande@ens.psl.eu>
Date: Thu, 26 Jun 2025 17:15:24 +0200
Subject: [PATCH 06/28] builders

---
 HB/builders.elpi | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/HB/builders.elpi b/HB/builders.elpi
index 4c4ea543b..0aa91533a 100644
--- a/HB/builders.elpi
+++ b/HB/builders.elpi
@@ -90,7 +90,7 @@ declare-shadowed-constant (some C) :-
 
 pred declare-shadowed-located i:string, i:located.
 declare-shadowed-located Id (loc-gref GR) :-
-  @global! => log.coq.notation.add-abbreviation Id 0 (global GR) ff _.
+  @global! => log.coq.notation.add-abbreviation Id 0 {coq.env.global GR} ff _.
 declare-shadowed-located Id (loc-abbreviation Abbrev) :-
   coq.notation.abbreviation-body Abbrev NArgs T,
   @global! => log.coq.notation.add-abbreviation Id NArgs T ff _.
@@ -103,7 +103,7 @@ postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [
   Msg is "Unable to declare factory " ^ Name,
   std.assert-ok! (coq.typecheck-ty Package _) Msg,
   log.coq.env.add-section-variable-noimplicits Name Package C,
-  TheFactory = global (const C),
+  coq.env.global (const C) TheFactory,
 ].
 
 % Only record fields can be exported as operations.
@@ -121,14 +121,14 @@ define-factory-operation TheType Params TheFactory NHoles (some P) :-
   coq.mk-n-holes NHoles Holes,
   std.append Holes [TheFactory] Holes_Factory,
   std.append Params [TheType|Holes_Factory] Args,
-  T = app[global (const P)|Args],
+  T = app[{coq.env.global (const P)}|Args],
   std.assert-ok! (coq.typecheck T _) "Illtyped applied factory operation",
   coq.gref->id (const P) Name,
   @local! => log.coq.notation.add-abbreviation Name 0 T ff _.
 
 pred factory i:context-decl, o:string, o:gref.
 factory (context-item IDF _ T _ _\ context-end) IDF GR :- !,
-  coq.safe-dest-app T (global GR) _.
+  coq.safe-dest-global-app T GR _.
 factory (context-item _ _ _ _ R) IDF GR :- !, pi x\ factory (R x) IDF GR.
 factory _ _ _ :- !, coq.error "the last context item is not a factory".
 
@@ -146,4 +146,4 @@ postulate-factories ModName IDF CDecl :- std.do! [
   acc-clause current (current-mode (builder-from FKey TheFactory GRF ModName)),
 ].
 
-}
\ No newline at end of file
+}

From fd4e106a3cb94aba9be4ffcb6a970280dbda9992 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Thu, 26 Jun 2025 17:23:59 +0200
Subject: [PATCH 07/28] database

---
 HB/common/database.elpi | 33 +++++++++++++++++----------------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index 425a8b525..8869e26e4 100644
--- a/HB/common/database.elpi
+++ b/HB/common/database.elpi
@@ -12,7 +12,7 @@ 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).
+from_builder (from _ _ GR) X :- coq.env.global GR X.
 
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
@@ -59,7 +59,7 @@ instance-to-export_instance-nice (instance-to-export _ M _) M.
 pred abbrev-to-export_name i:prop, o:id.
 abbrev-to-export_name (abbrev-to-export _ N _) N.
 pred abbrev-to-export_body i:prop, o:term.
-abbrev-to-export_body (abbrev-to-export _ _ B) (global B).
+abbrev-to-export_body (abbrev-to-export _ _ GR) B :- coq.env.global GR B.
 
 pred clause-to-export_clause i:prop, o:prop.
 clause-to-export_clause (clause-to-export _ C) C.
@@ -110,11 +110,13 @@ factory-provides.one Params T B M (triple M PL T) :- std.do! [
 pred extract-conclusion-params i:term, i:term, o:list term.
 extract-conclusion-params TheType (prod _ S T) R :- !,
   @pi-decl _ S x\ extract-conclusion-params TheType (T x) R.
-extract-conclusion-params TheType (app [global GR|Args]) R :- !, std.do! [
+extract-conclusion-params TheType Tm R :-
+  coq.safe-dest-global-app Tm GR Args, !, std.do! [
   std.assert-ok! (factory-alias->gref GR Factory) "HB",
   factory-nparams Factory NP,
   std.map Args (copy-pack-holes TheType TheType) NewArgs,
-  std.take NP NewArgs R].
+  std.take NP NewArgs R
+  ].
 extract-conclusion-params TheType T R :- whd1 T T1, !, extract-conclusion-params TheType T1 R.
 
 
@@ -311,22 +313,23 @@ assert-good-coverage! MLSortedRev CNL :- std.do! [
 
 % [get-structure-coercion S1 S2 F] finds the coecion F from the structure S1 to S2
 pred get-structure-coercion i:structure, i:structure, o:term.
-get-structure-coercion S T (global F) :-
+get-structure-coercion S T Out :-
   coq.coercion.db-for (grefclass S) (grefclass T) L,
-  if (L = [pr F _]) true (coq.error "No one step coercion from" S "to" T).
+  if (L = [pr F _]) true (coq.error "No one step coercion from" S "to" T),
+  coq.env.global F Out.
 
 pred get-structure-sort-projection i:structure, o:term.
 get-structure-sort-projection (indt S) Proj :- !,
   coq.env.projections S L,
   if (L = [some P, _]) true (coq.error "No canonical sort projection for" S),
-  Proj = global (const P).
+  coq.env.global (const P) Proj.
 get-structure-sort-projection S _ :- coq.error "get-structure-sort-projection: not a structure" S.
 
 pred get-structure-class-projection i:structure, o:term.
 get-structure-class-projection (indt S) T :- !,
   coq.env.projections S L,
   if (L = [_, some P]) true (coq.error "No canonical class projection for" S),
-  T = global (const P).
+  coq.env.global (const P) T.
 get-structure-class-projection S _ :- coq.error "get-structure-class-projection: not a structure" S.
 
 pred get-constructor i:gref, o:gref.
@@ -350,18 +353,16 @@ has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).
 
 
 pred mixin-src->has-mixin-instance i:prop, o:prop.
-mixin-src->has-mixin-instance  (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
-  term->gref I IHd.
-
-mixin-src->has-mixin-instance (mixin-src (app [global GR|_] ) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
-  term->gref I IHd.
-
 mixin-src->has-mixin-instance (mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd):-
   term->gref I IHd.
 
 mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):-
   term->gref I IHd.
 
+mixin-src->has-mixin-instance  (mixin-src Src M I) (has-mixin-instance (cs-gref GR) M IHd) :- !,
+  coq.safe-dest-global-app Src GR _, !, term->gref I IHd.
+
+
 % this auxiliary function iterates over the list of arguments of an application,
 % and create the necessary unify condition for each arguments
 % and at the end returns the mixin-src clause with all the conditions
@@ -402,7 +403,7 @@ mixin-instance-type->mixin-src (prod N_ _ F) M I Cond (pi a \ C a) :-
 
 pred has-mixin-instance->mixin-src i:prop, o:prop.
 has-mixin-instance->mixin-src (has-mixin-instance _ M IHd) C :- std.do![
-  T = global IHd,
+  coq.env.global IHd T,
   coq.env.typeof IHd Ty,
   mixin-instance-type->mixin-src Ty M T [] C,
 ].
@@ -437,7 +438,7 @@ structure-nparams Structure NParams :-
 pred factory? i:term, o:w-args factoryname.
 factory? S (triple F Params T) :-
   not (var S), !,
-  safe-dest-app S (global GR) Args,
+  coq.safe-dest-global-app S GR Args,
   factory-alias->gref GR F ok,
   factory-nparams F NP, !,
   std.split-at NP Args Params [T|_].

From 3eca8fdfc5495a3ae1835e72667116e6e79353b1 Mon Sep 17 00:00:00 2001
From: qvermande <quentin.vermande@ens.psl.eu>
Date: Thu, 26 Jun 2025 17:15:24 +0200
Subject: [PATCH 08/28] instance structure

---
 HB/instance.elpi  | 41 +++++++++++++++++++----------------
 HB/structure.elpi | 54 +++++++++++++++++++++++++----------------------
 2 files changed, 52 insertions(+), 43 deletions(-)

diff --git a/HB/instance.elpi b/HB/instance.elpi
index 063b4fe09..9e1b08eea 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -11,7 +11,7 @@ declare-existing T0 F0 :- std.do! [
   argument->term F0 F,
   std.assert-ok! (coq.typecheck F FTy)
     "HB: declare-existing illtyped factory instance",
-  std.assert! (coq.safe-dest-app FTy (global FactoryAlias) _)
+  std.assert! (coq.safe-dest-global-app FTy FactoryAlias _)
      "The type of the instance is not a factory",
   std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB: ",
   private.declare-instance Factory T F Clauses _ _,
@@ -42,7 +42,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
   ),
 
   % identify the factory
-  std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory",
+  std.assert! (coq.safe-dest-global-app SectionTy FactoryAlias Args) "The type of the instance is not a factory",
   std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB",
   std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB",
 
@@ -67,7 +67,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
 
   log.coq.env.add-const-noimplicits-failondup RealName OptimizedBody
     SectionTyUnfolded @transparent! C,
-  TheFactory = (global (const C)),
+  coq.env.global (const C) TheFactory,
 
   private.check-non-forgetful-inheritance TheType Factory,
 
@@ -171,7 +171,7 @@ infer-class T  Class Struct MLwP S Name STy Clauses:- std.do![
   get-constructor Struct KS,
   coq.safe-dest-app T THD _,
   private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses,
-  coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S,
+  coq.mk-app {coq.env.global KS} {std.append Params [T, KCAppNames]} S,
   if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}),
 
   coq.typecheck S STy ok, % failure may be due to a parameter not rich enough see #435
@@ -212,7 +212,8 @@ saturate-instances Filter :- std.do! [
 
 pred no-instance-for i:cs-pattern, i:class.
 no-instance-for K (class _ S _) :-
-  get-structure-sort-projection S (global Proj),
+  get-structure-sort-projection S G,
+  coq.env.global Proj G,
   coq.CS.db-for Proj K [].
 
 /* ------------------------------------------------------------------------- */
@@ -249,22 +250,25 @@ add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do
   new_int N, % timestamp
 
   synthesis.assert!-infer-mixin T MissingMixin Bo,
-  MixinSrcCl = mixin-src T MixinName (global (const C)),
-  BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)),
 
   std.assert-ok! (coq.typecheck Bo Ty) "declare-instances: mixin illtyped",
-  safe-dest-app Ty (global MixinNameAlias) _,
+  coq.safe-dest-global-app Ty MixinNameAlias _,
   std.assert-ok! (factory-alias->gref MixinNameAlias MixinName) "HB",
 
   std.assert! (MissingMixin = MixinName) "HB: anomaly: we built the wrong mixin",
 
   % If the mixin instance is already a constant there is no need to
   % alias it.
-  if (Bo = global (const C)) true
+  if (coq.env.global (const C) Bo) true
     (Name is {gref->modname FGR 2 "_"} ^"__to__" ^ {gref->modname MixinName 2 "_"},
      if-verbose (coq.say {header} "declare mixin instance" Name),
      log.coq.env.add-const-noimplicits Name Bo Ty @transparent! C),
-  if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _)
+
+  coq.env.global (const C) G,
+  MixinSrcCl = mixin-src T MixinName G,
+  BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)),
+
+  if (MakeCanon = tt, whd {coq.env.global (const C)} [] X _, coq.env.global (indc _) X)
      (std.do! [
          if-verbose (coq.say {header} "declare canonical mixin instance" C),
          with-locality (log.coq.CS.declare-instance C),
@@ -292,7 +296,7 @@ postulate-arity (parameter ID _ S A) Acc T T1 Ty :-
   if-verbose (coq.say {header} "postulating" ID),
   if (var S) (coq.fresh-type S) true,
   log.coq.env.add-section-variable-noimplicits ID S C,
-  Var = global (const C),
+  coq.env.global (const C) Var,
   postulate-arity (A Var) [Var|Acc] T T1 Ty.
 postulate-arity (arity Ty) ArgsRev X T Ty :-
   hd-beta X {std.rev ArgsRev} X1 Stack1,
@@ -348,7 +352,7 @@ hack-section-discharging B B.
 % unfolds the constant used for the phant abbreviation to avoid storing all
 % the phantom abstrctions and idfun that were used to trigger inference
 pred optimize-body i:term, o:term.
-optimize-body (app[global (const C)| Args]) Red :- (phant-abbrev _ (const C) _ ; (rex_match "phant_" {coq.gref->id (const C)})), !,
+optimize-body (app[Hd| Args]) Red :- coq.env.global (const C) Hd, (phant-abbrev _ (const C) _ ; (rex_match "phant_" {coq.gref->id (const C)})), !,
   coq.env.const C (some B) _,
   hd-beta B Args HD Stack,
   unwind HD Stack Red.
@@ -362,7 +366,7 @@ hnf X X.
 pred optimize-class-body i:term, i:int, i:term, o:term, o:list prop.
 optimize-class-body T NParams (let _ _ MBo R) R1 Clauses :- std.do! [
   declare-mixin-name {hnf MBo} MC CL1,
-  if (T = global (indt _), MC = global (const C), not(coq.env.opaque? C))
+  if (coq.env.global (indt _) T, coq.env.global (const C) MC, not(coq.env.opaque? C))
      (log.coq.strategy.set [C] (level 1000)) true, % opaque stops simpl
   optimize-class-body T NParams (R MC) R1 CL2,
   std.append CL1 CL2 Clauses,
@@ -370,20 +374,21 @@ optimize-class-body T NParams (let _ _ MBo R) R1 Clauses :- std.do! [
 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 (global (const C)) [mixin-mem T (const C)] :- std.do! [
+declare-mixin-name T T [] :- coq.env.global _ T.
+declare-mixin-name T G [] :- mixin-mem T GR, coq.env.global GR G.
+declare-mixin-name T T [] :- coq.safe-dest-global-app T GR _, not (from _ _ GR), not (get-option "hnf" tt).
+declare-mixin-name T G [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}),
   log.coq.env.add-const-noimplicits Name T _ @transparent! C,
+  coq.env.global (const C) G
 ].
 
 pred check-non-forgetful-inheritance i:term, i:gref.
 check-non-forgetful-inheritance _ _ :-
   get-option "non_forgetful_inheritance" tt, !.
 check-non-forgetful-inheritance T Factory :- std.do! [
-  if (coq.safe-dest-app T (global (const HdSym)) _, structure-key HdSym _ Super) (
+  if (coq.safe-dest-global-app T (const HdSym) _, structure-key HdSym _ Super) (
     coq.warning "HB" "HB.non-forgetful-inheritance"
       "non forgetful inheritance detected.\n"
       "You have two solutions:"
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 3702ce191..b72a3418d 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -87,9 +87,9 @@ declare Module BSkel Sort :- std.do! [
   if (get-option "short.type" ShortType) (
     if-verbose (coq.say {header} "short name for type:" ShortType),
     (@global! => log.coq.notation.add-abbreviation
-      ShortType 0 (global Structure) ff _)) true,
+      ShortType 0 {coq.env.global Structure} ff _)) true,
 
-  coq.mk-app (global Structure) {coq.mk-n-holes {w-params.nparams MLwP}} HB_Instance,
+  coq.mk-app {coq.env.global Structure} {coq.mk-n-holes {w-params.nparams MLwP}} HB_Instance,
   if (get-option "short.pack" ShortPack) (std.do! [
     if-verbose (coq.say {header} "declaring pack abbreviation:" ShortPack),
     % coq.notation.abbreviation-body PackAbbrev NPackAbbrev PackAbbrevTrm,
@@ -106,7 +106,7 @@ declare Module BSkel Sort :- std.do! [
   if-verbose (coq.say {header} "making coercion from type to target"),
   synthesis.infer-coercion-tgt MLwP CoeClass,
   if-arg-sort (private.declare-sort-coercion CoeClass Structure
-    (global (const ArgSortCst))),
+    {coq.env.global (const ArgSortCst)}),
   private.declare-sort-coercion CoeClass Structure SortProjection,
 
   if-verbose (coq.say {header} "exporting unification hints"),
@@ -138,14 +138,14 @@ declare Module BSkel Sort :- std.do! [
 
   if-verbose (coq.say {header} "declaring on_ abbreviation"),
 
-  private.mk-infer-key CoeClass ClassProjection NilwP (global Structure) PhClass,
+  private.mk-infer-key CoeClass ClassProjection NilwP {coq.env.global Structure} PhClass,
 
   phant.add-abbreviation "on_" PhClass _ ClassOfAbbrev,
   (pi c\ coq.notation.abbreviation ClassOfAbbrev [c] (ClassOfAbbrev_ c)),
 
   if-verbose (coq.say {header} "declaring `copy` abbreviation"),
 
-  coq.mk-app (global ClassName) {params->holes NilwP} AppClassHoles,
+  coq.mk-app {coq.env.global ClassName} {params->holes NilwP} AppClassHoles,
   @global! => log.coq.notation.add-abbreviation "copy" 2
     {{fun T C => (lp:(ClassOfAbbrev_ C) : (lp:AppClassHoles T)) }} tt _,
 
@@ -204,9 +204,11 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
   gref-deps (const Po) MLwP,
   w-params.nparams MLwP NParams,
   std.length {list-w-params_list MLwP} NMixins,
+  coq.env.global (const Po) G,
+  coq.env.global (const C) GC,
 
   (pi L L1 L2 Params Rest PoArgs\
-    copy (app [global (const Po)| L]) (app [global (const C) | L2]) :-
+    copy (app [G| L]) (app [GC | L2]) :-
       std.split-at NParams L Params [_|Rest],
       std.drop NMixins Rest PoArgs,
       std.append Params [S|PoArgs] L1,
@@ -216,7 +218,7 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
 pred operation-body-and-ty i:list prop, i:constant, i:structure, i:term, i:term,
   i:list term, i:term, i:w-args A, o:pair term term.
 operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ ParamsOp _) (pr Bo Ty) :- std.do! [
-  mk-app (global Struct) Params StructType,
+  mk-app {coq.env.global Struct} Params StructType,
   mk-app Psort Params PsortP,
   mk-app Pclass Params PclassP,
   Bo = fun `s` StructType Body,
@@ -284,14 +286,14 @@ pred mk-coe-class-body
   i:list (w-args mixinname),
   o:term.
 mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [
-  mk-app (global FC) {std.append Params [T]} Class,
+  mk-app {coq.env.global FC} {std.append Params [T]} Class,
 
   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 (x\r\ sigma G\ coq.env.global x G, mk-app G Params r) BuildersP,
 
   factory-nparams TC TCNP,
-  mk-app (global {get-constructor TC})
+  mk-app {coq.env.global {get-constructor TC}}
     {coq.mk-n-holes TCNP} KCHoles,
 
   (pi c\ sigma Mixes\
@@ -314,13 +316,13 @@ pred mk-coe-structure-body
 mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection
     Params _T _ SCoeBody :- std.do! [
 
-  mk-app (global StructureF) Params StructureP,
+  mk-app {coq.env.global StructureF} Params StructureP,
   mk-app     SortProjection  Params SortP,
   mk-app     ClassProjection Params ClassP,
   mk-app     Coercion        Params CoercionP,
 
   factory-nparams TC TCNP,
-  mk-app (global {get-constructor StructureT})
+  mk-app {coq.env.global {get-constructor StructureT}}
     {coq.mk-n-holes TCNP} PackPH,
 
   SCoeBody = {{ fun s : lp:StructureP =>
@@ -351,7 +353,7 @@ declare-coercion SortProjection ClassProjection
   log.coq.env.add-const-noimplicits CName CoeBody' Ty @transparent! C,
   log.coq.coercion.declare (coercion (const C) 1 FC (grefclass TC)),
 
-  Coercion = global (const C),
+  coq.env.global (const C) Coercion,
   w-params.then FMLwP mk-fun ignore
     (mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection)
     SCoeBody,
@@ -374,7 +376,7 @@ pred join-body i:int, i:int, i:structure, i:term, i:term, i:term, i:term, i:term
   i:list term, i:name, i:term, i:(term -> A), o:term.
 join-body N1 N2 S3 S2_Pack S1_sort S3_to_S1 S2_class S3_to_S2
   P N _Ty _F (fun N S3P Pack) :- !,
-  mk-app (global S3) P S3P, !,
+  mk-app {coq.env.global S3} P S3P, !,
   @pi-decl N S3P s\
   sigma S3_to_S1_Ps S3_to_S2_Ps S1_sortS3Ps S2_classS3Ps Holes1 Holes2 \ std.do! [
     coq.mk-n-holes N2 Holes2,
@@ -402,7 +404,7 @@ declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C
 
   if-verbose (coq.say {header} "declare unification hint" Name),
   w-params.fold MLwP3 mk-fun (join-body N1 N2 S3
-    (global S2_Pack) S1_sort S3_to_S1 S2_class S3_to_S2) JoinBody,
+    {coq.env.global S2_Pack} S1_sort S3_to_S1 S2_class S3_to_S2) JoinBody,
   std.assert-ok! (coq.typecheck JoinBody Ty) "declare-join: JoinBody illtyped",
   log.coq.env.add-const-noimplicits Name JoinBody Ty @transparent! J,
   log.coq.CS.declare-instance J.
@@ -445,7 +447,8 @@ pred mk-record+sort-field i:sort, i:name, i:term, i:(term -> record-decl), o:ind
 mk-record+sort-field Sort _ T F (record "type" (sort Sort) "Pack" (field _ "sort" T F)).
 
 pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl.
-mk-class-field ClassName Params T _ (field [canonical ff] "class" (app [global ClassName|Args]) _\end-record) :-
+mk-class-field ClassName Params T _ (field [canonical ff] "class" (app [G|Args]) _\end-record) :-
+  coq.env.global ClassName G,
   std.append Params [T] Args.
 
 % Builds the axioms record and the factories from this class to each mixin
@@ -481,13 +484,14 @@ declare-class+structure MLwP Sort
     (log.coq.env.add-indt StructureDeclaration StructureInd),
 
   coq.env.projections StructureInd [some SortP, some ClassP],
-  global (const SortP) = SortProjection,
-  global (const ClassP) = ClassProjection,
+  coq.env.global (const SortP) SortProjection,
+  coq.env.global (const ClassP) ClassProjection,
 ].
 
 % Declares "sort" as a Coercion Proj : Structurename >-> CoeClass.
 pred declare-sort-coercion i:class, i:structure, i:term.
-declare-sort-coercion CoeClass StructureName (global Proj) :-
+declare-sort-coercion CoeClass StructureName G :-
+  coq.env.global Proj G,
 
   if-verbose (coq.say {header} "declare sort coercion"),
 
@@ -516,14 +520,14 @@ mc-compat-structure ModuleName _Module NewMixins CNParams ClassProjection GRPack
   log.coq.env.begin-module ModuleName none,
 
   if (Axioms = some GR)
-    (@global! => log.coq.notation.add-abbreviation "axiom" 0 (global GR) ff _)
+    (@global! => log.coq.notation.add-abbreviation "axiom" 0 {coq.env.global GR} ff _)
     true,
 
   if (NewMixins = [NewMixin]) (std.do! [
     if-verbose (coq.say "mc-compat-structure: declaring notations 'axioms', 'mixin_of' and 'Mixin'"),
     factory-nparams NewMixin NewMixinNP,
     MArgs is NewMixinNP + 1,
-    mk-eta MArgs {coq.env.typeof NewMixin} (global NewMixin) EtaNewMixin,
+    mk-eta MArgs {coq.env.typeof NewMixin} {coq.env.global NewMixin} EtaNewMixin,
     @global! => log.coq.notation.add-abbreviation "axioms" MArgs EtaNewMixin ff _,
     @deprecated! "mathcomp 2.0.0" "use the factory instead" =>
     @global! => log.coq.notation.add-abbreviation "mixin_of" MArgs EtaNewMixin ff _,
@@ -553,10 +557,10 @@ mc-compat-structure ModuleName _Module NewMixins CNParams ClassProjection GRPack
 pred clone-phant-body i:factoryname, i:term, i:structure, i:list term, i:term, i:list (w-args mixinname), o:phant-term.
 clone-phant-body ClassName SortProjection ((indt I) as Structure) PL T _ PhF :- std.do! [
   std.assert! (coq.env.indt I _ _ _ _ [PackC] _) "wtf",
-  mk-app (global (indc PackC)) {std.append PL [T]} PackPLT,
-  mk-app (global Structure) PL SPL,
+  mk-app {coq.env.global (indc PackC)} {std.append PL [T]} PackPLT,
+  mk-app {coq.env.global Structure} PL SPL,
   (@pi-decl `cT` SPL cT\
-  mk-app (global ClassName) {std.append PL [T]} CPL,
+  mk-app {coq.env.global ClassName} {std.append PL [T]} CPL,
   @pi-decl `c` CPL c\
   (Ph cT c) =
     {phant.fun-unify none T {mk-app {mk-app SortProjection PL} [cT]}
@@ -578,7 +582,7 @@ pack-body ClassName PL T MLwA F :- std.do! [
 ].
 pack-body.aux PL T BuildC PackS  Body :- !, std.do! [
   synthesis.infer-all-gref-deps PL T BuildC Class,
-  mk-app (global PackS) {std.append PL [T, Class]} Body
+  mk-app {coq.env.global PackS} {std.append PL [T, Class]} Body
 ].
 
 pred mk-infer-key i:class, i:term, i:mixins, i:term, o:phant-term.

From aa9b5ed303c8b35ea389ccfb7121b9f7f0093a31 Mon Sep 17 00:00:00 2001
From: qvermande <quentin.vermande@ens.psl.eu>
Date: Thu, 26 Jun 2025 17:27:30 +0200
Subject: [PATCH 09/28] stdpp synthesis structures

---
 HB/common/stdpp.elpi     | 18 ++++++++--------
 HB/common/synthesis.elpi | 44 ++++++++++++++++++++++------------------
 HB/structures.v          |  2 +-
 3 files changed, 35 insertions(+), 29 deletions(-)

diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index 9264603d1..405d46052 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -147,8 +147,7 @@ constraint print-ctx mixin-src {
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 pred coq.term-is-gref? i:term, o:gref.
-coq.term-is-gref? (global GR) GR :- !.
-coq.term-is-gref? (pglobal GR _) GR :- !.
+coq.term-is-gref? G GR :- coq.env.global GR G, !.
 coq.term-is-gref? (app [Hd|_]) GR :- !, coq.term-is-gref? Hd GR.
 coq.term-is-gref? (let _ _ T x\x) GR :- !, coq.term-is-gref? T GR.
 
@@ -220,8 +219,9 @@ coq.abstract-indt-decl [C|CS] X (parameter ID explicit Ty1 X1) :-
   coq.gref->id (const C) ID,
   coq.env.typeof (const C) Ty,
   copy Ty Ty1,
+  coq.env.global (const C) G,
   @pi-parameter ID Ty x\
-    (copy (global (const C)) x :- !) =>
+    (copy G x :- !) =>
     coq.abstract-indt-decl CS X (X1 x).
 
 % [coq.abstract-const-decl Section I AbsI] abstracts I over the Section variables
@@ -233,8 +233,9 @@ coq.abstract-const-decl [C|CS] X (pr (fun Name Ty1 X1) (prod Name Ty1 X2)) :-
   coq.id->name ID Name,
   coq.env.typeof (const C) Ty,
   copy Ty Ty1,
+  coq.env.global (const C) G,
   @pi-parameter ID Ty x\
-    (copy (global (const C)) x :- !) =>
+    (copy G x :- !) =>
     coq.abstract-const-decl CS X (pr (X1 x) (X2 x)).
 
 % [coq.copy-clauses-for-unfold CS CL] generates clauses for the copy predicate
@@ -243,21 +244,22 @@ pred coq.copy-clauses-for-unfold i:list constant, o:list prop.
 coq.copy-clauses-for-unfold [] [].
 coq.copy-clauses-for-unfold [C|CS] [ClauseApp,Clause|L] :-
   coq.env.const C (some B) _,
+  coq.env.global (const C) G,
   ClauseApp = (pi B1 Args Args1 B2 Args2 R\
-    copy (app[global (const C)|Args]) R :- !,
+    copy (app[G|Args]) R :- !,
       copy B B1,
       std.map Args copy Args1,
       hd-beta B1 Args1 B2 Args2,
       unwind B2 Args2 R),
   Clause = (pi B1\
-    copy (global (const C)) B1 :- !, copy B B1),
+    copy G B1 :- !, copy B B1),
   coq.copy-clauses-for-unfold CS L.
 
 % like fold-map, needed for coq-elpi < 1.9
 
 pred coq.fold-map i:term, i:A, o:term, o:A.
 coq.fold-map X A Y A :- name X, !, X = Y, !. % avoid loading "coq.fold-map x A x A" at binders
-coq.fold-map (global _ as C) A C A :- !.
+coq.fold-map C A C A :- coq.env.global _ C, !.
 coq.fold-map (sort _ as C) A C A :- !.
 coq.fold-map (fun N T F) A (fun N T1 F1) A2 :- !,
   coq.fold-map T A T1 A1, pi x\ coq.fold-map (F x) A1 (F1 x) A2.
@@ -360,4 +362,4 @@ constraint seen? seen! purge-seen!  {
   rule purge-seen! \ (seen! _ _).
   rule \ purge-seen!.
 }
-}
\ No newline at end of file
+}
diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi
index 6444e23c2..64e3b3db3 100644
--- a/HB/common/synthesis.elpi
+++ b/HB/common/synthesis.elpi
@@ -30,7 +30,7 @@ infer-all-gref-deps Ps T GR X :- std.do! [
   std.assert! (gref-deps GR MLwP) "BUG: gref-deps should never fail",
   list-w-params_list MLwP ML,
   coq.env.typeof GR Ty,
-  coq.mk-eta (-1) Ty (global GR) EtaF,
+  coq.mk-eta (-1) Ty {coq.env.global GR} EtaF,
   coq.subst-fun {std.append Ps [T]} EtaF FT,
   private.instantiate-all-these-mixin-args FT T ML Xraw,
   infer-holes-depending-on-params T Xraw X,
@@ -38,17 +38,18 @@ infer-all-gref-deps Ps T GR X :- std.do! [
 
 % [infer-holes-depending-on-params TheType T NewT]
 pred infer-holes-depending-on-params i:term, i:term, o:term.
-infer-holes-depending-on-params T (app [global GR|Args]) (app [global GR|Args1]) :- !,
+infer-holes-depending-on-params T (app [G|Args]) (app [G|Args1]) :-
+  coq.env.global _ G, !,
   std.map Args (infer-holes-depending-on-pack T) Args1.
 infer-holes-depending-on-params _ X X.
 
 pred class-of-phant i:term, o:gref, o:gref, o:gref.
 class-of-phant (prod N T F) X Y Z :- @pi-decl N T x\ class-of-phant (F x) X Y Z.
-class-of-phant (global GR) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z.
-class-of-phant (app[global GR|_]) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z.
+class-of-phant T Y Z X :- coq.safe-dest-global-app T GR _, class-def (class X GR _), get-constructor X Y, get-constructor GR Z.
 
 pred infer-holes-depending-on-pack i:term, i:term, o:term.
-infer-holes-depending-on-pack T (app [global GR | Args]) S :-
+infer-holes-depending-on-pack T (app [G | Args]) S :-
+  coq.env.global GR G,
   ((coq.gref->id GR GRS, rex.match "phant.*" GRS /*TODO: phant-clone? GR N*/);
     pack? GR _),
   coq.env.typeof GR Ty, class-of-phant Ty KC SC C,
@@ -57,19 +58,19 @@ infer-holes-depending-on-pack T (app [global GR | Args]) S :-
   std.do! [
     infer-all-args-let Params T KC ClassInstance ok,
     std.rev [ClassInstance,T|{std.rev Params}] NewArgs,
-    S = app[global SC| NewArgs ]
+    S = app[{coq.env.global SC}| NewArgs ]
   ].
 infer-holes-depending-on-pack _ X X.
 
 % [infer-all-args-let Ps T GR X Diagnostic] fills in all the Args in
-%   app[global GR, Ps, T | Args]
+%   app[{coq.env.global GR}, Ps, T | Args]
 % and generates a term
-%   let `a1` ty1 t1 a1\ .... app[global GR, p1, .. pn, T, a1, .. , an]
+%   let `a1` ty1 t1 a1\ .... app[{coq.env.global GR}, p1, .. pn, T, a1, .. , an]
 % if Diagnostic is ok, else X is unassigned
 pred infer-all-args-let i:list term, i:term, i:gref, o:term, o:diagnostic.
 infer-all-args-let Ps T GR X Diag :- std.do! [
   coq.env.typeof GR Ty,
-  coq.mk-eta (-1) Ty (global GR) EtaF,
+  coq.mk-eta (-1) Ty {coq.env.global GR} EtaF,
   coq.subst-fun {std.append Ps [T]} EtaF FT,
   private.instantiate-all-args-let FT T X Diag,
 ].
@@ -205,14 +206,17 @@ drop 0 L L :- !.
 drop N [_|XS] L :- !, N1 is N - 1, drop N1 XS L.
 
 pred compress-copy o:term, o:term.
-compress-copy (app [global (const C) | L]) R :-
+compress-copy (app [G | L]) R :-
   sub-class C2 C3 C NparamsC,
-  drop NparamsC L [app [global (const C') | L']],
+  coq.env.global (const C) G,
+  drop NparamsC L [app [G' | L']],
   sub-class C1 C2 C' NparamsC',
+  coq.env.global (const C') G',
   drop NparamsC' L' L'',
   sub-class C1 C3 C'' NparamsC'',
   std.append {coq.mk-n-holes NparamsC''} L'' HL'',
-  CHL'' = app [global (const C'') | HL''],
+  CHL'' = app [G'' | HL''],
+  coq.env.global (const C'') G'',
   coq.typecheck CHL'' _ ok, !,
   compress-copy CHL'' R.
 compress-copy (app L) (app L1) :- !, std.map L compress-copy L1.
@@ -234,7 +238,7 @@ mixin-for_mixin-builder (mixin-for _ _ B) B.
 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,
-  F = global FGR,
+  coq.env.global FGR F,
   gref-deps Src MLwP,
   list-w-params_list MLwP ML,
   infer-all-these-mixin-args Ps T ML F B,
@@ -248,7 +252,7 @@ builder->term Ps T Src Tgt B :- !, std.do! [
 % thus instanciating an abstraction on mixin M_i with X_i
 pred instantiate-all-these-mixin-args i:term, i:term, i:list mixinname, o:term.
 instantiate-all-these-mixin-args (fun _ Tm F) T ML R :-
-  coq.safe-dest-app Tm (global TmGR) _,
+  coq.safe-dest-global-app Tm TmGR _,
   factory-alias->gref TmGR M ok,
   std.mem! ML M,
   !,
@@ -260,7 +264,7 @@ instantiate-all-these-mixin-args F _ _ F.
 
 pred instantiate-all-args-let i:term, i:term, o:term, o:diagnostic.
 instantiate-all-args-let (fun N Tm F) T (let N Tm X R) Diag :- !, std.do! [
-  coq.safe-dest-app Tm (global TmGR) _,
+  coq.safe-dest-global-app Tm TmGR _,
   factory-alias->gref TmGR M ok,
   if (mixin-for T M X)
      (@pi-def N Tm X m\ instantiate-all-args-let (F m) T (R m) Diag)
@@ -281,18 +285,18 @@ structure-instance->mixin-srcs T S MSLC :- std.do! [
   structure-nparams S NParams,
   coq.mk-n-holes NParams Holes,
   std.append Holes [ST] HolesST,
-  coq.mk-app (global (const SortProj)) HolesST SortHolesST,
+  coq.mk-app {coq.env.global (const SortProj)} HolesST SortHolesST,
   % find an instance in ST
   coq.unify-eq T SortHolesST ok,
   % we look for an instance which is concrete, we take the parts
   get-constructor S KS,
-  coq.mk-app (global KS) {std.append Holes [T, CT]} KSHolesC,
+  coq.mk-app {coq.env.global KS} {std.append Holes [T, CT]} KSHolesC,
   coq.unify-eq ST KSHolesC ok,
   % if the class instance is concrete, we take the parts
   get-constructor (indt Class) KC,
   std.length {list-w-params_list CMLwP} CMixinsN,
   coq.mk-n-holes CMixinsN MIL,
-  coq.mk-app (global KC) {std.append Holes [T | MIL]} CBody,
+  coq.mk-app {coq.env.global KC} {std.append Holes [T | MIL]} CBody,
   coq.unify-eq CT CBody ok,
   % we finally generare micin-src clauses for all mixins
   std.map MIL (structure-instance->mixin-srcs.aux T) MSLL,
@@ -304,7 +308,7 @@ structure-instance->mixin-srcs T S MSLC :- std.do! [
 structure-instance->mixin-srcs _ _ [].
 
 structure-instance->mixin-srcs.aux2 Params T Class (some P) M :-
-  coq.mk-app (global (const P)) {std.append Params [T,Class]} M.
+  coq.mk-app {coq.env.global (const P)} {std.append Params [T,Class]} M.
 structure-instance->mixin-srcs.aux T  F CL :-
   factory-instance->new-mixins [] F ML,
   std.map-filter ML (m\c\ not (mixin-src T m _), c = mixin-src T m F) CL.
@@ -315,7 +319,7 @@ structure-instance->mixin-srcs.aux T  F CL :-
 pred factory-instance->new-mixins i:list mixinname, i:term, o:list mixinname.
 factory-instance->new-mixins OldMixins X NewML :- std.do! [
   std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped",
-  if (not (coq.safe-dest-app XTy (global _) _))
+  if (not (coq.safe-dest-global-app XTy _ _))
      (coq.error "Term:\n" {coq.term->string X}
                 "\nhas type:\n" {coq.term->string XTy}
                 "\nwhich is not a record")
diff --git a/HB/structures.v b/HB/structures.v
index 112084d7b..865f51fb7 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -132,7 +132,7 @@ pred factory-alias->gref i:gref, o:gref, o: diagnostic.
 factory-alias->gref PhGR GR ok :- phant-abbrev GR PhGR _, !.
 factory-alias->gref GR GR ok :- phant-abbrev GR _ _, !.
 factory-alias->gref GR _ (error Msg) :- !,
-  Msg is {coq.term->string (global GR)} ^
+  Msg is {coq.term->string {coq.env.global GR} } ^
          " is not a factory or its library (" ^
         { std.string.concat "." {std.drop-last 1 {coq.gref->path GR} } } ^
         ") was not correctly imported".

From d05c5daffba733814a1e80665b9dd7be7789a4f9 Mon Sep 17 00:00:00 2001
From: qvermande <quentin.vermande@ens.psl.eu>
Date: Thu, 26 Jun 2025 22:44:18 +0200
Subject: [PATCH 10/28] phant-abbreviation (I think we did everything)

---
 HB/common/phant-abbreviation.elpi | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/HB/common/phant-abbreviation.elpi b/HB/common/phant-abbreviation.elpi
index 943c30c74..cc9b803a9 100644
--- a/HB/common/phant-abbreviation.elpi
+++ b/HB/common/phant-abbreviation.elpi
@@ -24,7 +24,7 @@ add-abbreviation N (private.phant-term AL T1) C Abbrev :- std.do! [
   NC is "phant_" ^ N,
   std.assert-ok! (coq.elaborate-skeleton T1 TTy T) "add-abbreviation: T illtyped",
   log.coq.env.add-const-noimplicits NC T TTy @transparent! C,
-  private.build-abbreviation 0 (global (const C)) AL NParams AbbrevT,
+  private.build-abbreviation 0 {coq.env.global (const C)} AL NParams AbbrevT,
   @global! => log.coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
 ].
 
@@ -39,7 +39,7 @@ pred of-gref i:bool, i:gref, i:list mixinname, o:phant-term.
 of-gref WithCopy GRF RealMixinArgs PhBody:- !, std.do! [
   std.assert! (gref-deps GRF MLwP) "mk-phant-term: unknown gref",
   std.assert! (coq.env.typeof GRF FTy) "mk-phant-term: F illtyped",
-  coq.mk-eta (-1) FTy (global GRF) EtaF,
+  coq.mk-eta (-1) FTy {coq.env.global GRF} EtaF,
   % toposort-mixins ML MLSorted,
   MLwP = MLwPSorted, % Assumes we give them already sorted in dep order.
   std.rev {list-w-params_list MLwPSorted} MLSortedRev,
@@ -139,13 +139,13 @@ phant-fun Arg Ty PhF (phant-term [Arg|ArgL] (fun N Ty F)) :-
 pred phant-fun-mixin i:name, i:term, i:(term -> phant-term), o:phant-term.
 phant-fun-mixin N Ty PF (private.phant-term [Status|AL] (fun N Ty F)) :- !, std.do! [
   @pi-decl N Ty t\ PF t = private.phant-term AL (F t),
-  coq.safe-dest-app Ty (global Mixin) _,
+  coq.safe-dest-global-app Ty Mixin _,
   if (this-mixin-is-real-arg Mixin) (Status = private.real N) (Status = private.implicit)
 ].
 
 pred fun-unify-mixin i:term, i:name, i:term, i:(term -> phant-term), o:phant-term.
 fun-unify-mixin T N Ty PF Out :- !, std.do! [
-  coq.safe-dest-app Ty (global M) _,
+  coq.safe-dest-global-app Ty M _,
   Msg is "fun-unify-mixin: No mixin-src on " ^ {coq.term->string T},
   std.assert! (mixin-src T M Msrc) Msg,
   (@pi-decl `m` Ty m\ fun-unify none m Msrc (PF m) (PFM m)),
@@ -158,7 +158,7 @@ fun-unify-mixin T N Ty PF Out :- !, std.do! [
 pred phant-fun-struct i:term, i:name, i:structure, i:list term, i:(term -> phant-term), o:phant-term.
 phant-fun-struct T Name S Params PF Out :- std.do! [
   get-structure-sort-projection S SortProj,
-  mk-app (global S) Params SParams,
+  mk-app {coq.env.global S} Params SParams,
   mk-app SortProj Params SortProjParams,
   % Msg = {{lib:hb.nomsg}},
   Msg = some {{lp:SParams}},
@@ -199,7 +199,7 @@ pred build-type-pattern i:gref, o:term.
 build-type-pattern GR Pat :- build-type-pattern.aux GR {coq.env.typeof GR} Pat.
 build-type-pattern.aux GR T {{ lp:Pat _ }} :- coq.unify-eq T (prod N S T') ok, !,
   @pi-decl N S x\ build-type-pattern.aux GR (T' x) Pat.
-build-type-pattern.aux GR T (global GR) :- coq.unify-eq T {{ Type }} ok, !.
+build-type-pattern.aux GR T G :- coq.unify-eq T {{ Type }} ok, !, coq.env.global GR G.
 build-type-pattern.aux _ _ _ :- coq.error "HB: wrong carrier type".
 
 
@@ -237,13 +237,13 @@ pred mk-phant-term.mixins i:term, i:term, i:classname, i:phant-term,
   i:list term, i:name, i:term, i:(term -> list (w-args mixinname)), o:phant-term.
 mk-phant-term.mixins Target Src CN PF Params N Ty MLwA Out :- std.do! [
   class-def (class CN SI _),
-  mk-app (global SI) Params SIParams,
+  mk-app {coq.env.global SI} Params SIParams,
   coq.name-suffix N "local" Nlocal,
   (@pi-decl Nlocal Ty t\ sigma SK KC ML ParamsT SKPT\ std.do! [
     std.map (MLwA t) triple_1 ML,
     std.append Params [t] ParamsT,
-    SKPT = app [global {get-constructor SI} | ParamsT],
-    ClassTy t = app [global CN | ParamsT],
+    SKPT = app [{coq.env.global {get-constructor SI} } | ParamsT],
+    ClassTy t = app [{coq.env.global CN} | ParamsT],
     (@pi-decl `s` SIParams s\ @pi-decl `c` (ClassTy t) c\ sigma PF2\ std.do![
        synthesis.under-mixins.then (MLwA t) (fun-unify-mixin Target)
           (mk-phant-term.mixins.aux t Params c CN PF) PF2,

From e325ab9e614dfec377b99978f99686d1ca6ef3ac Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Fri, 27 Jun 2025 01:29:10 +0200
Subject: [PATCH 11/28] upoly-* wip

---
 HB/factory.elpi               | 36 ++++++++++++++++++++++++++++++-----
 HB/structures.v               | 12 +++++++++++-
 _CoqProject.test-suite        |  1 +
 tests/polymorphic_universes.v |  5 +++++
 4 files changed, 48 insertions(+), 6 deletions(-)
 create mode 100644 tests/polymorphic_universes.v

diff --git a/HB/factory.elpi b/HB/factory.elpi
index c1ecc639f..a7cdda982 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -28,10 +28,18 @@ argument->w-mixins (indt-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
   pdecl->w-mixins Decl (pr MLwP DeclwP),
   w-params.map DeclwP (_\ _\ x\ y\ y = indt-decl x) ArgwP
 ].
+argument->w-mixins (upoly-indt-decl Decl UI) (pr MLwP ArgwP) :- !, std.do! [
+  pdecl->w-mixins Decl (pr MLwP DeclwP),
+  w-params.map DeclwP (_\ _\ x\ y\ y = upoly-indt-decl x UI) ArgwP
+].
 argument->w-mixins (const-decl Id none Decl) (pr MLwP ArgwP) :- !, std.do! [
   pdecl->w-mixins Decl (pr MLwP DeclwP),
   w-params.map DeclwP (_\ _\ x\ y\ y = const-decl Id none x) ArgwP,
 ].
+argument->w-mixins (upoly-const-decl Id none Decl UI) (pr MLwP ArgwP) :- !, std.do! [
+  pdecl->w-mixins Decl (pr MLwP DeclwP),
+  w-params.map DeclwP (_\ _\ x\ y\ y = upoly-const-decl Id none x UI) ArgwP,
+].
 argument->w-mixins (const-decl Id (some Body) Decl as CDecl)
     (pr MLwP ArgwP) :- !, std.do! [
   if-verbose (coq.say {header} "arguments->w-mixins on const-decl Decl=" CDecl),
@@ -46,17 +54,35 @@ argument->w-mixins (const-decl Id (some Body) Decl as CDecl)
     coq.subst-fun Args Body AppBody,
     y = const-decl Id (some AppBody) x]) ArgwP
 ].
+argument->w-mixins (upoly-const-decl Id (some Body) Decl UI as CDecl)
+    (pr MLwP ArgwP) :- !, std.do! [
+  if-verbose (coq.say {header} "arguments->w-mixins on const-decl Decl=" CDecl),
+  pdecl->w-mixins Decl (pr MLwP DeclwP),
+  if-verbose (coq.say {header} "arguments->w-mixins on const-decl Decl=" Decl
+    "\nwith MLwP =" MLwP),
+  std.length {list-w-params_list MLwP} NML,
+  if-verbose (coq.say "ML length =" NML),
+  w-params.map DeclwP (ps\ t\ x\ y\ sigma Dummies Args AppBody\ std.do! [
+    std.nlist NML (sort prop) Dummies,
+    std.append ps [t|Dummies] Args,
+    coq.subst-fun Args Body AppBody,
+    y = upoly-const-decl Id (some AppBody) x UI]) ArgwP
+].
 argument->w-mixins (ctx-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
   cdecl->w-mixins Decl (pr MLwP DeclwP),
   w-params.map DeclwP (_\ _\ x\ y\ y = ctx-decl x) ArgwP
 ].
 
+pred indt-decl-name i:indt-decl, o:string.
+indt-decl-name (parameter _ _ _ R) Id :- !, indt-decl-name (R (sort prop)) Id.
+indt-decl-name (record Id _ _ _) Id :- !.
+indt-decl-name (inductive Id _ _ _) Id :- !.
+
 pred argument-name i:argument, o:string.
 argument-name (const-decl Id _ _) Id :- !.
-argument-name (indt-decl (parameter _ _ _ R)) Id :- !,
-argument-name (indt-decl (R (sort prop))) Id.
-argument-name (indt-decl (record Id _ _ _)) Id :- !.
-argument-name (indt-decl (inductive Id _ _ _)) Id :- !.
+argument-name (upoly-const-decl Id _ _ _) Id :- !.
+argument-name (indt-decl Decl) Id :- !, indt-decl-name Decl Id.
+argument-name (upoly-indt-decl Decl _) Id :- !, indt-decl-name Decl Id.
 argument-name (ctx-decl _) "_" :- !.
 
 pred pdecl->w-mixins i:indt-decl, o:w-mixins indt-decl.
@@ -214,7 +240,7 @@ declare-asset Arg AssetKind :- std.do! [
   if-verbose (coq.say {header} "declaring context" FLwP),
   context.declare FLwP MLwP Params TheKey MixinSrcClauses SectionCanonicalInstance,
 
-  if (Arg = indt-decl _) (
+  if (Arg = indt-decl _; Arg = upoly-indt-decl _ _) (
     apply-w-params ArgwP Params TheKey (indt-decl (record _ Sort _ Fields)),
     if-verbose (coq.say {header} "declare mixin or factory"),
     declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
diff --git a/HB/structures.v b/HB/structures.v
index 865f51fb7..dcbe499df 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -487,7 +487,8 @@ actions N :-
   coq.env.current-library File,
   coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File E)).
 
-main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).
+main [indt-decl D] :- !, record-decl->id D N, with-attributes (actions N).
+main [upoly-indt-decl D _] :- !, coq.say D, record-decl->id D N, coq.say N, with-attributes (actions N).
 
 main _ :-
   coq.error "Usage: HB.mixin Record <MixinName> T of F A & … := { … }.".
@@ -654,6 +655,7 @@ main [const-decl N (some B) Arity] :- std.do! [
   if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort,
   with-attributes (with-logging (structure.declare N B Univ)),
 ].
+main [upoly-const-decl N (some B) Arity _] :- main [const-decl N (some B) Arity].
 
 }}.
 #[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
@@ -692,6 +694,7 @@ actions-compat ModuleName :-
   true.
 
 main [const-decl N _ _] :- !, with-attributes (actions N).
+main [upoly-const-decl N _ _ _] :- !, with-attributes (actions N).
 
 main _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
 }}.
@@ -779,6 +782,8 @@ Elpi Accumulate lp:{{
 :name "start"
 main [const-decl Name (some BodySkel) TyWPSkel] :- !,
   with-attributes (with-logging (instance.declare-const Name BodySkel TyWPSkel _ _)).
+main [upoly-const-decl Name (some BodySkel) TyWPSkel _] :- !,
+  with-attributes (with-logging (instance.declare-const Name BodySkel TyWPSkel _ _)).
 main [T0, F0] :- !,
   coq.warning "HB" "HB.deprecated" "The syntax \"HB.instance Key FactoryInstance\" is deprecated, use \"HB.instance Definition\" instead",
   with-attributes (with-logging (instance.declare-existing T0 F0)).
@@ -792,6 +797,10 @@ main [const-decl _ _ (arity _)] :- !.
 main [const-decl _ _ (parameter _ _ _ _)] :- !,
   SectionName is "hb_instance_" ^ {std.any->string {new_int} },
   begin-section SectionName, end-section.
+main [upoly-const-decl _ _ (arity _) _] :- !.
+main [upoly-const-decl _ _ (parameter _ _ _ _) _] :- !,
+  SectionName is "hb_instance_" ^ {std.any->string {new_int} },
+  begin-section SectionName, end-section.
 main [_, _] :- !.
 
 main _ :- coq.error "Usage: HB.instance Definition <Name> := <Builder> T ...".
@@ -844,6 +853,7 @@ actions N :-
   coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File E)).
 
 main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).
+main [upoly-indt-decl D _] :- record-decl->id D N, with-attributes (actions N).
 main [const-decl N _ _] :- with-attributes (actions N).
 
 main _ :-
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
index 31c827eb4..a1100a3c0 100644
--- a/_CoqProject.test-suite
+++ b/_CoqProject.test-suite
@@ -50,6 +50,7 @@ tests/two_hier.v
 tests/instance_merge_with_param.v
 tests/instance_merge_with_distinct_param.v
 tests/instance_merge.v
+tests/polymorphic_universes.v
 
 tests/unit/enrich_type.v
 tests/unit/mixin_src_has_mixin_instance.v
diff --git a/tests/polymorphic_universes.v b/tests/polymorphic_universes.v
new file mode 100644
index 000000000..f0e59f2dc
--- /dev/null
+++ b/tests/polymorphic_universes.v
@@ -0,0 +1,5 @@
+From HB Require Import structures.
+Set Universe Polymorphism.
+
+HB.mixin Record isA T := {}.
+HB.structure Definition A := {T of isA T}.

From 73bd3deb74e93686e1e839fd1c642905c4dc0189 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Fri, 27 Jun 2025 15:21:40 +0200
Subject: [PATCH 12/28] upoly-* wip

compiles by miracle, but does not produce univ polymorphic records...
---
 HB/factory.elpi | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index a7cdda982..3df9f49d8 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -28,17 +28,17 @@ argument->w-mixins (indt-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
   pdecl->w-mixins Decl (pr MLwP DeclwP),
   w-params.map DeclwP (_\ _\ x\ y\ y = indt-decl x) ArgwP
 ].
-argument->w-mixins (upoly-indt-decl Decl UI) (pr MLwP ArgwP) :- !, std.do! [
+argument->w-mixins (upoly-indt-decl Decl _UI) (pr MLwP ArgwP) :- !, std.do! [
   pdecl->w-mixins Decl (pr MLwP DeclwP),
-  w-params.map DeclwP (_\ _\ x\ y\ y = upoly-indt-decl x UI) ArgwP
+  w-params.map DeclwP (_\ _\ x\ y\ y = indt-decl x) ArgwP % TODO: investigate, looks fishy!
 ].
 argument->w-mixins (const-decl Id none Decl) (pr MLwP ArgwP) :- !, std.do! [
   pdecl->w-mixins Decl (pr MLwP DeclwP),
   w-params.map DeclwP (_\ _\ x\ y\ y = const-decl Id none x) ArgwP,
 ].
-argument->w-mixins (upoly-const-decl Id none Decl UI) (pr MLwP ArgwP) :- !, std.do! [
+argument->w-mixins (upoly-const-decl Id none Decl _UI) (pr MLwP ArgwP) :- !, std.do! [
   pdecl->w-mixins Decl (pr MLwP DeclwP),
-  w-params.map DeclwP (_\ _\ x\ y\ y = upoly-const-decl Id none x UI) ArgwP,
+  w-params.map DeclwP (_\ _\ x\ y\ y = const-decl Id none x) ArgwP, % TODO: investigate, looks fishy!
 ].
 argument->w-mixins (const-decl Id (some Body) Decl as CDecl)
     (pr MLwP ArgwP) :- !, std.do! [
@@ -54,7 +54,7 @@ argument->w-mixins (const-decl Id (some Body) Decl as CDecl)
     coq.subst-fun Args Body AppBody,
     y = const-decl Id (some AppBody) x]) ArgwP
 ].
-argument->w-mixins (upoly-const-decl Id (some Body) Decl UI as CDecl)
+argument->w-mixins (upoly-const-decl Id (some Body) Decl _UI as CDecl)
     (pr MLwP ArgwP) :- !, std.do! [
   if-verbose (coq.say {header} "arguments->w-mixins on const-decl Decl=" CDecl),
   pdecl->w-mixins Decl (pr MLwP DeclwP),
@@ -66,7 +66,7 @@ argument->w-mixins (upoly-const-decl Id (some Body) Decl UI as CDecl)
     std.nlist NML (sort prop) Dummies,
     std.append ps [t|Dummies] Args,
     coq.subst-fun Args Body AppBody,
-    y = upoly-const-decl Id (some AppBody) x UI]) ArgwP
+    y = const-decl Id (some AppBody) x]) ArgwP % TODO: investigate, looks fishy!
 ].
 argument->w-mixins (ctx-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
   cdecl->w-mixins Decl (pr MLwP DeclwP),

From 833719a390b9f4790fac9b90cad22f3b5afc4fa1 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Tue, 1 Jul 2025 18:13:54 +0200
Subject: [PATCH 13/28] forcing univ poly + using appropriate PR

---
 .nix/config.nix   | 57 ++++++++++++++++++++++++++++++++---------------
 HB/factory.elpi   |  5 ++---
 HB/structure.elpi |  6 ++---
 HB/structures.v   |  1 +
 4 files changed, 45 insertions(+), 24 deletions(-)

diff --git a/.nix/config.nix b/.nix/config.nix
index 821e7c498..aa96df726 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -2,7 +2,7 @@
   format = "1.0.0";
   attribute = "hierarchy-builder";
   no-rocq-yet = true;
-  default-bundle = "coq-8.20";
+  default-bundle = "coq-universes-clauses";
   bundles = let
     mcHBcommon = {
       mathcomp.override.version = "master";
@@ -29,23 +29,44 @@
       simple-io.override.version = "master";
       QuickChick.override.version = "master";
       # jasmin.override.version = "main";
-      jasmin.job = false;  # currently broken
+      jasmin.job = false; # currently broken
     };
   in {
-    "coq-master" = { rocqPackages = {
-      rocq-core.override.version = "master";
-      stdlib.override.version = "master";
-      rocq-elpi.override.version = "master";
-      rocq-elpi.override.elpi-version = "2.0.7";
-      bignums.override.version = "master";
-    }; coqPackages = mcHBcommon // {
-      coq.override.version = "master";
-      stdlib.override.version = "master";
-      coq-elpi.override.version = "master";
-      coq-elpi.override.elpi-version = "2.0.7";
-      bignums.override.version = "master";
-      coquelicot.job = false;
-    }; };
+    "coq-universes-clauses" = {
+      rocqPackages = {
+        rocq-core.override.version = "mattam82:universes-clauses";
+        stdlib.override.version = "master";
+        rocq-elpi.override.version = "mattam82:universes-clauses";
+        rocq-elpi.override.elpi-version = "2.0.7";
+        bignums.override.version = "master";
+      };
+      coqPackages = mcHBcommon // {
+        coq.override.version = "mattam82:universes-clauses";
+        stdlib.override.version = "master";
+        coq-elpi.override.version = "mattam82:universes-clauses";
+        coq-elpi.override.elpi-version = "2.0.7";
+        bignums.override.version = "master";
+        coquelicot.job = false;
+      };
+    };
+
+    "coq-master" = {
+      rocqPackages = {
+        rocq-core.override.version = "master";
+        stdlib.override.version = "master";
+        rocq-elpi.override.version = "master";
+        rocq-elpi.override.elpi-version = "2.0.7";
+        bignums.override.version = "master";
+      };
+      coqPackages = mcHBcommon // {
+        coq.override.version = "master";
+        stdlib.override.version = "master";
+        coq-elpi.override.version = "master";
+        coq-elpi.override.elpi-version = "2.0.7";
+        bignums.override.version = "master";
+        coquelicot.job = false;
+      };
+    };
 
     "coq-9.0".coqPackages = mcHBcommon // {
       coq.override.version = "9.0";
@@ -61,8 +82,8 @@
     };
 
   };
-  cachix.coq = {};
-  cachix.coq-community = {};
+  cachix.coq = { };
+  cachix.coq-community = { };
   cachix.math-comp.authToken = "CACHIX_AUTH_TOKEN";
 
 }
diff --git a/HB/factory.elpi b/HB/factory.elpi
index 3df9f49d8..1c68e555e 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -265,10 +265,9 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
-
   if (get-option "primitive" tt)
-    (@primitive! => log.coq.env.add-indt RDeclClosed R)
-    (log.coq.env.add-indt RDeclClosed R),
+    (@primitive! => @univpoly! => log.coq.env.add-indt RDeclClosed R)
+    (@univpoly! => log.coq.env.add-indt RDeclClosed R),
 
   log.coq.env.end-section-name Module, % We need to anyway declare the record inside the section
     % since closing the section purges the unused universe level we may have
diff --git a/HB/structure.elpi b/HB/structure.elpi
index b72a3418d..5550c6ac5 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -463,7 +463,7 @@ declare-class+structure MLwP Sort
     synthesize-fields.body ClassDeclaration,
 
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
-  (@primitive! => log.coq.env.add-indt ClassDeclaration ClassInd),
+  (@univpoly! => @primitive! => log.coq.env.add-indt ClassDeclaration ClassInd),
 
   coq.env.projections ClassInd Projs,
   % TODO: put this code in a named clause
@@ -480,8 +480,8 @@ declare-class+structure MLwP Sort
 
   std.assert-ok! (coq.typecheck-indt-decl StructureDeclaration) "declare: illtyped",
   if (get-option "primitive" tt)
-    (@primitive! => log.coq.env.add-indt StructureDeclaration StructureInd)
-    (log.coq.env.add-indt StructureDeclaration StructureInd),
+    (@univpoly! => @primitive! => log.coq.env.add-indt StructureDeclaration StructureInd)
+    (@univpoly! => log.coq.env.add-indt StructureDeclaration StructureInd),
 
   coq.env.projections StructureInd [some SortP, some ClassP],
   coq.env.global (const SortP) SortProjection,
diff --git a/HB/structures.v b/HB/structures.v
index dcbe499df..79dde2f81 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -1,5 +1,6 @@
 (* Support constants, to be kept in sync with shim/structures.v *)
 From Corelib Require Import ssreflect ssrfun.
+Set Universe Polymotphism.
 
 Variant error_msg := NoMsg | IsNotCanonicallyA (x : Type).
 Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : error_msg) :=

From b3957efde3b53ef1c517741e81556a0e52d0a2cf Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Tue, 1 Jul 2025 18:29:37 +0200
Subject: [PATCH 14/28] Adding experiments

---
 experiments.v | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 experiments.v

diff --git a/experiments.v b/experiments.v
new file mode 100644
index 000000000..21bdf95de
--- /dev/null
+++ b/experiments.v
@@ -0,0 +1,42 @@
+From elpi Require Import elpi.
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Module test_rocq.
+Record test : Type := mktest { foo : Type }.
+Print test. (* Record test@{u} : Type@{u+1} := mktest { foo : Type@{u} }. (* u |=  *)*)
+End test_rocq.
+
+Module test_elpi.
+Elpi Command test_default.
+Elpi Query lp:"
+   coq.env.add-indt (record ""test"" {{Type}} ""mktest""
+     (field _ ""foo"" {{Type}}  _ \ end-record)) _C.
+".
+Print test. (* Record test : Type@{test.u0} := mktest { foo : Type@{test.u1} }. *)
+(* we get a monomorphic universe *)
+End test_elpi.
+
+Module test_explicit.
+Elpi Command test_explicit.
+Elpi Query lp:"
+   @keep-alg-univs! => @univpoly! => coq.env.add-indt (record ""test"" {{Type}} ""mktest""
+     (field _ ""foo"" {{Type}}  _ \ end-record)) _C.
+".
+Print test.
+(* Record test@{u u0} : Type@{u} := mktest { foo : Type@{u0} }. *)
+(* u(= (* for typing) in term, + in type) u0(= in term) |= u0 < u *) *)
+(* It's indeed polymorphic but we do not get the minimized version *)
+End test_explicit.
+
+Module test_minimization.
+Elpi Command test_minimization.
+Elpi Query lp:"
+   coq.univ.new U,
+   coq.univ.variable U V,
+   @keep-alg-univs! => @udecl! [V] ff [] tt => coq.env.add-indt (record ""test"" (sort (typ _)) ""mktest""
+     (field _ ""foo"" (sort (typ U))  _ \ end-record)) _C.
+".
+Print test.
+(* It's indeed polymorphic but we do not get the minimized version *))
+End test_minimization.

From 3067c41e15ea320b5e30c469aa93df893a1fbcc5 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Thu, 17 Jul 2025 10:42:23 +0200
Subject: [PATCH 15/28] debugging

---
 HB/common/log.elpi |  8 ++++----
 HB/factory.elpi    | 14 ++++++++++++--
 HB/structure.elpi  | 11 +++++++----
 examples/readme.v  | 10 +++++++---
 4 files changed, 30 insertions(+), 13 deletions(-)

diff --git a/HB/common/log.elpi b/HB/common/log.elpi
index 134f9eecb..f4f074612 100644
--- a/HB/common/log.elpi
+++ b/HB/common/log.elpi
@@ -35,7 +35,7 @@ env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
   avoid-name-collision Name Name1,
-  coq.env.add-const Name1 Bo Ty Opaque C,
+  @univpoly! => coq.env.add-const Name1 Bo Ty Opaque C,
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
   log.private.log-vernac (log.private.coq.vernac.definition Name1 Ty? Bo),
@@ -49,7 +49,7 @@ env.add-const Name Bo Ty Opaque C :- std.do! [
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
   avoid-name-collision Name Name1,
-  coq.env.add-const Name1 Bo Ty Opaque C,
+  @univpoly! => coq.env.add-const Name1 Bo Ty Opaque C,
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
   log.private.log-vernac (log.private.coq.vernac.definition Name1 Ty? Bo),
@@ -61,7 +61,7 @@ env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [
     (coq.error "HB: cannot infer some information in" Name
                ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
     true,
-  coq.env.add-const Name Bo Ty Opaque C,
+  @univpoly! => coq.env.add-const Name Bo Ty Opaque C,
   env.add-location (const C),
   if (var Ty) (Ty? = none) (Ty? = some Ty),
   log.private.log-vernac (log.private.coq.vernac.definition Name Ty? Bo),
@@ -79,7 +79,7 @@ env.add-indt Decl I :- std.do! [
   if (not(coq.ground-indt-decl? Decl))
     (coq.error "HB: cannot infer some information in" {coq.indt-decl->string Decl})
     true,
-  coq.env.add-indt Decl I,
+  (@univpoly! => coq.env.add-indt Decl I),
   (coq.env.record? I P ; P = ff),
   log.private.log-vernac (log.private.coq.vernac.inductive Decl P),
   env.add-location (indt I),
diff --git a/HB/factory.elpi b/HB/factory.elpi
index 1c68e555e..3443893b2 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -265,9 +265,15 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
+  coq.say "ZZZZZZZZZZ",
+  std.assert-ok! (coq.typecheck-indt-decl RDeclClosed) "RDeclClosed: illtyped",
+
   if (get-option "primitive" tt)
-    (@primitive! => @univpoly! => log.coq.env.add-indt RDeclClosed R)
-    (@univpoly! => log.coq.env.add-indt RDeclClosed R),
+    (@primitive! => log.coq.env.add-indt RDeclClosed R)
+    (log.coq.env.add-indt RDeclClosed R),
+
+  coq.say TheType,
+  coq.say RDeclClosed,
 
   log.coq.env.end-section-name Module, % We need to anyway declare the record inside the section
     % since closing the section purges the unused universe level we may have
@@ -340,7 +346,11 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
   std.assert-ok! (coq.elaborate-ty-skeleton Ty1Skel _ Ty1) "Illtyped alias factory",
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr Ty1 _) (pr Ty1Closed _) Section,
+  std.assert-ok! (coq.typecheck Ty1Closed _) "Typechecking of Ty1Closed failed",
+  coq.say "YYYYYYY",
+  coq.say {coq.term->string Ty1Closed},
   log.coq.env.add-const-noimplicits "axioms_" Ty1Closed _ @transparent! C,
+  coq.say {coq.term->string {coq.env.global (const C)}},
 
   std.assert! (coq.safe-dest-global-app Ty1 PhF _Args) "Argument must be a factory",
   std.assert-ok! (factory-alias->gref PhF F) "HB",
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 5550c6ac5..537b24514 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -64,7 +64,10 @@ declare Module BSkel Sort :- std.do! [
   (ClassAlias => class-def CurrentClass => GRDepsClauses => MixinMems =>
     w-params.then MLwP mk-fun mk-fun (private.pack-body ClassName) Pack),
   if-verbose (coq.say {header} "declaring pack_ constant =" Pack),
+  coq.say {coq.term->string Pack},
+  std.assert-ok! (coq.typecheck Pack _) "typechecking failure: pack_",
   log.coq.env.add-const-noimplicits "pack_" Pack _ @transparent! ConstPack,
+  coq.say "XXXXX",
   GRPack = const ConstPack,
 
   if-arg-sort (
@@ -457,13 +460,13 @@ declare-class+structure MLwP Sort
     (indt ClassInd) (indt StructureInd) SortProjection ClassProjection AllFactories
     (structure-key SortP ClassP (indt StructureInd)):- std.do! [
 
-  if-verbose (coq.say {header} "declare axioms record"MLwP ),
+  if-verbose (coq.say {header} "declare axioms record" MLwP),
 
   w-params.then MLwP (mk-parameter explicit) (mk-parameter explicit)
     synthesize-fields.body ClassDeclaration,
 
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
-  (@univpoly! => @primitive! => 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
@@ -480,8 +483,8 @@ declare-class+structure MLwP Sort
 
   std.assert-ok! (coq.typecheck-indt-decl StructureDeclaration) "declare: illtyped",
   if (get-option "primitive" tt)
-    (@univpoly! => @primitive! => log.coq.env.add-indt StructureDeclaration StructureInd)
-    (@univpoly! => log.coq.env.add-indt StructureDeclaration StructureInd),
+    (@primitive! => log.coq.env.add-indt StructureDeclaration StructureInd)
+    (log.coq.env.add-indt StructureDeclaration StructureInd),
 
   coq.env.projections StructureInd [some SortP, some ClassP],
   coq.env.global (const SortP) SortProjection,
diff --git a/examples/readme.v b/examples/readme.v
index f2a45edd0..4009fc2e4 100644
--- a/examples/readme.v
+++ b/examples/readme.v
@@ -1,20 +1,24 @@
 From HB Require Import structures.
 From Corelib Require Import ssreflect BinNums IntDef.
+Set Printing Universes.
+Set Universe Polymorphism.
+Unset Printing Records.
 
-#[verbose, log]
-HB.mixin Record AddComoid_of_Type A := {
+#[verbose]
+HB.mixin Record AddComoid_of_Type (A : Type) := {
   zero : A;
   add : A -> A -> A;
   addrA : forall x y z, add x (add y z) = add (add x y) z;
   addrC : forall x y, add x y = add y x;
   add0r : forall x, add zero x = x;
 }.
-#[verbose, log(raw)]
 HB.structure Definition AddComoid := { A of AddComoid_of_Type A }.
 
 Notation "0" := zero.
 Infix "+" := add.
 
+About AddComoid_of_Type.axioms_.
+
 Check forall (M : AddComoid.type) (x : M), x + x = 0.
 
 HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid_of_Type A := {

From f8a587ab61da091e119e1708f80a839fa65235ef Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Fri, 18 Jul 2025 17:57:28 +0200
Subject: [PATCH 16/28] various fixes

---
 HB/common/phant-abbreviation.elpi |  8 +++++++-
 HB/common/stdpp.elpi              |  6 ++++++
 HB/common/synthesis.elpi          |  2 ++
 HB/common/utils.elpi              |  5 -----
 HB/factory.elpi                   | 12 +++---------
 HB/instance.elpi                  |  3 ++-
 HB/structure.elpi                 | 20 ++++++++++++--------
 HB/structures.v                   |  2 +-
 8 files changed, 33 insertions(+), 25 deletions(-)

diff --git a/HB/common/phant-abbreviation.elpi b/HB/common/phant-abbreviation.elpi
index cc9b803a9..a26ba642a 100644
--- a/HB/common/phant-abbreviation.elpi
+++ b/HB/common/phant-abbreviation.elpi
@@ -257,17 +257,21 @@ mk-phant-term.mixins Target Src CN PF Params N Ty MLwA Out :- std.do! [
 ].
 
 mk-phant-term.mixins.aux T Params C CN PF X :- std.do![
+  coq.say "entering mk-phant-term.mixins.aux" CN KC,
   get-constructor CN KC,
   synthesis.infer-all-gref-deps Params T KC KCM,
   fun-unify none KCM C PF X,
+  coq.say "exiting mk-phant-term.mixins.aux" CN X,
 ].
 
 pred mk-phant-term.class
   i:term, i:term, i:classname, i:phant-term, o:phant-term.
 mk-phant-term.class Target Src CN PF CPF :- !, std.do! [
   class-def (class CN _ CMLwP),
+  coq.say "Class Hit:" CN CMLwP,
   w-params.fold CMLwP fun-implicit
     (mk-phant-term.mixins Target Src CN PF) CPF,
+  coq.say "Class Folded!"
 ].
 
 pred mk-phant-term.classes
@@ -277,7 +281,9 @@ mk-phant-term.classes EtaF CNF PL Target Src MLwA PhF :- !, std.do! [
   std.map MLwA triple_1 ML,
   synthesis.under-mixins.then MLwA phant-fun-mixin (out\ sigma FPLTM\ std.do! [
     synthesis.infer-all-these-mixin-args PL Target ML EtaF FPLTM,
-    std.fold CNF (phant-term [] FPLTM) (mk-phant-term.class Target Src) out]) PhF
+    coq.say "MID-PHANT-TERM-CLASSES",
+    std.fold CNF (phant-term [] FPLTM) (mk-phant-term.class Target Src) out]) PhF,
+    coq.say "FOLDED!"
 ].
 
 pred mk-phant-term-with-copy i:term, i:list classname,
diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index 405d46052..4cbbca92c 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -300,6 +300,12 @@ cs-pattern->name (cs-sort _) "sort".
 cs-pattern->name cs-default "default".
 cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name.
 
+% decompose [app (p?global X UI?)|Args] into X and Args, using @univdecl UI to store UI.
+pred coq.safe-dest-global-app i:term, o:gref, o:list term.
+coq.safe-dest-global-app Tm GR Args :- !, std.do![
+    coq.safe-dest-app Tm Head Args, (Head = global GR; Head = pglobal GR _)
+  ].
+
 % ---------------------------------------------------------------------
 % kit for closing a term by abstracting evars with lambdas
 % we use constraints to attach to holes a number
diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi
index 64e3b3db3..39d960c54 100644
--- a/HB/common/synthesis.elpi
+++ b/HB/common/synthesis.elpi
@@ -17,10 +17,12 @@ namespace synthesis {
 % which are misxins in ML, abstracts the others
 pred infer-all-these-mixin-args i:list term, i:term, i:list mixinname, i:term, o:term.
 infer-all-these-mixin-args Ps T ML F SFX :- std.do! [
+  coq.say "SYNTH MIXINS = " Ps "," T "," ML "," F,
   std.assert-ok! (coq.typecheck F Ty) "try-infer-these-mixin-args: F illtyped",
   coq.mk-eta (-1) Ty F EtaF,
   coq.subst-fun {std.append Ps [T]} EtaF FT,
   private.instantiate-all-these-mixin-args FT T ML SFX,
+  coq.say "SYNTH MIXINS END"
 ].
 
 % [infer-all-gref-deps Ps T GR X] fills in all the arguments of GR
diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi
index 93c8d2039..ae4216b66 100644
--- a/HB/common/utils.elpi
+++ b/HB/common/utils.elpi
@@ -98,11 +98,6 @@ gref->modname_short1 MP S _ S :- string->modpath S MP.
 gref->modname_short1 MP S [X|L] S' :-
   gref->modname_short1 MP {std.string.concat "." [X,S]} L S'.
 
-pred coq.safe-dest-global-app i:term, o:gref, o:list term.
-coq.safe-dest-global-app Tm GR Args :- !, std.do![
-    coq.safe-dest-app Tm Head Args, coq.env.global GR Head
-  ].
-
 % Print shortest qualified identifier of the module containing a gref
 % Sep is used as separator
 pred gref->modname_short i:gref, i:string, o:string.
diff --git a/HB/factory.elpi b/HB/factory.elpi
index 3443893b2..64a2a0fac 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -263,18 +263,14 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   RDeclSkel = record "axioms_" Sort1 Kname Fields,
   std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclSkel RDecl) "record declaration illtyped",
 
-  abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
+  abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosedSkel _,
 
-  coq.say "ZZZZZZZZZZ",
-  std.assert-ok! (coq.typecheck-indt-decl RDeclClosed) "RDeclClosed: illtyped",
+  std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclClosedSkel RDeclClosed) "record declaration illtyped",
 
   if (get-option "primitive" tt)
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
     (log.coq.env.add-indt RDeclClosed R),
 
-  coq.say TheType,
-  coq.say RDeclClosed,
-
   log.coq.env.end-section-name Module, % We need to anyway declare the record inside the section
     % since closing the section purges the unused universe level we may have
     % allocated by typechecking the skeleton just above
@@ -297,6 +293,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   if-verbose (coq.say {header} "declare notation Build"),
 
   GRDepsClauses => phant.of-gref ff GRK [] PhGRK,
+  coq.say "XXXXXXX",
   GRDepsClauses => phant.add-abbreviation "Build" PhGRK BuildConst BuildAbbrev,
 
   if-verbose (coq.say {header} "declare notation axioms"),
@@ -347,10 +344,7 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr Ty1 _) (pr Ty1Closed _) Section,
   std.assert-ok! (coq.typecheck Ty1Closed _) "Typechecking of Ty1Closed failed",
-  coq.say "YYYYYYY",
-  coq.say {coq.term->string Ty1Closed},
   log.coq.env.add-const-noimplicits "axioms_" Ty1Closed _ @transparent! C,
-  coq.say {coq.term->string {coq.env.global (const C)}},
 
   std.assert! (coq.safe-dest-global-app Ty1 PhF _Args) "Argument must be a factory",
   std.assert-ok! (factory-alias->gref PhF F) "HB",
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 9e1b08eea..fd0d80a78 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -23,7 +23,7 @@ declare-existing T0 F0 :- std.do! [
 % that can be built using factory instance B. CFL contains the list of
 % factories being defined, CSL the list of canonical structures being defined.
 pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pair id constant).
-declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
+declare-const Name BodySkel TyWPSkel CFL CSL :- std.spy-do! [
   std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
   coq.arity->term TyWP Ty,
   std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",
@@ -65,6 +65,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
     (coq.error "HB: The instance subject must be explicitly given.\nUse:\n  HB.instance Definition _ : M <subject> := ...\n  HB.instance Definition _ := M.Build <subject> ...")
     true,
 
+  std.assert-ok! (coq.typecheck OptimizedBody _) "typechecking Optimized Body",
   log.coq.env.add-const-noimplicits-failondup RealName OptimizedBody
     SectionTyUnfolded @transparent! C,
   coq.env.global (const C) TheFactory,
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 537b24514..f7bd29087 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -64,10 +64,8 @@ declare Module BSkel Sort :- std.do! [
   (ClassAlias => class-def CurrentClass => GRDepsClauses => MixinMems =>
     w-params.then MLwP mk-fun mk-fun (private.pack-body ClassName) Pack),
   if-verbose (coq.say {header} "declaring pack_ constant =" Pack),
-  coq.say {coq.term->string Pack},
   std.assert-ok! (coq.typecheck Pack _) "typechecking failure: pack_",
   log.coq.env.add-const-noimplicits "pack_" Pack _ @transparent! ConstPack,
-  coq.say "XXXXX",
   GRPack = const ConstPack,
 
   if-arg-sort (
@@ -207,15 +205,21 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
   gref-deps (const Po) MLwP,
   w-params.nparams MLwP NParams,
   std.length {list-w-params_list MLwP} NMixins,
-  coq.env.global (const Po) G,
-  coq.env.global (const C) GC,
 
-  (pi L L1 L2 Params Rest PoArgs\
-    copy (app [G| L]) (app [GC | L2]) :-
+  % TODO: refactor
+  [(pi L L1 L2 Params Rest PoArgs\
+    (copy (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 L2)),
+   (pi UI L L1 L2 Params Rest PoArgs\
+    (copy (app [pglobal (const Po) UI | L]) (app [pglobal (const C) UI | L2]) :-
+      std.split-at NParams L Params [_|Rest],
+      std.drop NMixins Rest PoArgs,
+      std.append Params [S|PoArgs] L1,
+      std.map L1 copy L2))]
+  =>
   clean-op-ty Ops S T1 T2.
 
 pred operation-body-and-ty i:list prop, i:constant, i:structure, i:term, i:term,
@@ -249,7 +253,7 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std
 
   w-params.then MwP mk-fun-prod ignore (operation-body-and-ty EXI Poperation Struct Psort Pclass) (pr Body BodyTy),
 
-  if-verbose (coq.say {header} "export operation" Name),
+  if-verbose (coq.say {header} "export operation" Name "as" BodyTy),
   log.coq.env.add-const-noimplicits Name Body BodyTy @transparent! C,
 
   w-params.nparams MwP NP,
diff --git a/HB/structures.v b/HB/structures.v
index 79dde2f81..93abba10d 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -1,6 +1,6 @@
 (* Support constants, to be kept in sync with shim/structures.v *)
 From Corelib Require Import ssreflect ssrfun.
-Set Universe Polymotphism.
+Set Universe Polymorphism.
 
 Variant error_msg := NoMsg | IsNotCanonicallyA (x : Type).
 Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : error_msg) :=

From 0ecf331953f72d8fd3c8244b00bc78ffd8f38e51 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Mon, 15 Sep 2025 12:16:09 +0200
Subject: [PATCH 17/28] Debugging in progress

---
 HB/instance.elpi              |  4 +++-
 HB/structures.v               |  6 ++++--
 examples/readme.v             | 17 ++++++++++++++++-
 experiments.v                 |  9 ++++++---
 tests/polymorphic_universes.v |  7 ++++++-
 tests/unit/struct.v           |  3 +++
 6 files changed, 38 insertions(+), 8 deletions(-)

diff --git a/HB/instance.elpi b/HB/instance.elpi
index fd0d80a78..1e43b6be6 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -26,7 +26,9 @@ pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pai
 declare-const Name BodySkel TyWPSkel CFL CSL :- std.spy-do! [
   std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
   coq.arity->term TyWP Ty,
-  std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",
+  coq.say {coq.term->string Ty},
+  coq.say {coq.term->string BodySkel},
+  std.assert-ok! (coq.elaborate-skeleton BodySkel _ Body) "Definition illtyped WHYYYY?",
 
   % handle parameters via a section -- begin
   if (TyWP = arity SectionTy) (
diff --git a/HB/structures.v b/HB/structures.v
index 93abba10d..cd7b152bf 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -2,8 +2,10 @@
 From Corelib Require Import ssreflect ssrfun.
 Set Universe Polymorphism.
 
-Variant error_msg := NoMsg | IsNotCanonicallyA (x : Type).
-Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : error_msg) :=
+Variant phantom (T : Type) (p : T) : Prop :=  Phantom : phantom T p.
+
+Variant error_msg@{u} : Prop := NoMsg | IsNotCanonicallyA (x : Type@{u}).
+Definition unify@{u u'} (T1 T2 : Type@{u}) (t1 : T1) (t2 : T2) (s : error_msg@{u'}) :=
   phantom T1 t1 -> phantom T2 t2.
 Definition id_phant {T} {t : T} (x : phantom T t) := x.
 Definition id_phant_disabled {T T'} {t : T} {t' : T'} (x : phantom T t) := Phantom T' t'.
diff --git a/examples/readme.v b/examples/readme.v
index 4009fc2e4..e06c107a6 100644
--- a/examples/readme.v
+++ b/examples/readme.v
@@ -1,5 +1,5 @@
-From HB Require Import structures.
 From Corelib Require Import ssreflect BinNums IntDef.
+From HB Require Import structures.
 Set Printing Universes.
 Set Universe Polymorphism.
 Unset Printing Records.
@@ -12,21 +12,30 @@ HB.mixin Record AddComoid_of_Type (A : Type) := {
   addrC : forall x y, add x y = add y x;
   add0r : forall x, add zero x = x;
 }.
+#[verbose]
 HB.structure Definition AddComoid := { A of AddComoid_of_Type A }.
 
+About AddComoid_of_Type.axioms_.
+About AddComoid.type.
+
 Notation "0" := zero.
 Infix "+" := add.
 
 About AddComoid_of_Type.axioms_.
+About add.
+About addrA.
 
 Check forall (M : AddComoid.type) (x : M), x + x = 0.
 
+#[verbose, log(raw)]
 HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid_of_Type A := {
   opp : A -> A;
   addNr : forall x, opp x + x = 0;
 }.
 HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid A & }.
 
+About AbelianGrp_of_AddComoid.phant_Build.
+
 Notation "- x" := (opp x).
 
 Lemma example (G : AbelianGrp.type) (x : G) : x + (- x) = - 0.
@@ -37,7 +46,13 @@ Axiom Z_add_comm : forall x y, Z.add x y = Z.add y x.
 Axiom Z_add_0_l : forall x, Z.add Z0 x = x.
 Axiom Z_add_opp_diag_l : forall x, Z.add (Z.opp x) x = Z0.
 
+Fail #[verbose]
 HB.instance Definition Z_CoMoid := AddComoid_of_Type.Build Z Z0 Z.add Z_add_assoc Z_add_comm Z_add_0_l.
+Section test.
+Universe u u' u''.
+Check id_phant@{u+1} : unify@{u+1 max(u'+1,u'')}  Type@{u} Type@{u} Z _
+                         (is_not_canonically_a@{max(u'+1,u'')} AddComoid.type@{u' u''}).
+
 HB.instance Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z_add_opp_diag_l.
 
 Lemma example2 (x : Z) : x + (- x) = - 0.
diff --git a/experiments.v b/experiments.v
index 21bdf95de..74e04cf58 100644
--- a/experiments.v
+++ b/experiments.v
@@ -1,11 +1,14 @@
 From elpi Require Import elpi.
-Set Universe Polymorphism.
 Set Printing Universes.
 
 Module test_rocq.
-Record test : Type := mktest { foo : Type }.
+Section test.
+Variable A : Type.
+Record test : Type := mktest { foo : A }.
 Print test. (* Record test@{u} : Type@{u+1} := mktest { foo : Type@{u} }. (* u |=  *)*)
+End test.
 End test_rocq.
+Print test_rocq.test. (* Record test@{u} : Type@{u+1} := mktest { foo : Type@{u} }. (* u |=  *)*)
 
 Module test_elpi.
 Elpi Command test_default.
@@ -20,7 +23,7 @@ End test_elpi.
 Module test_explicit.
 Elpi Command test_explicit.
 Elpi Query lp:"
-   @keep-alg-univs! => @univpoly! => coq.env.add-indt (record ""test"" {{Type}} ""mktest""
+   @univpoly! => coq.env.add-indt (record ""test"" {{Type}} ""mktest""
      (field _ ""foo"" {{Type}}  _ \ end-record)) _C.
 ".
 Print test.
diff --git a/tests/polymorphic_universes.v b/tests/polymorphic_universes.v
index f0e59f2dc..d89afba3e 100644
--- a/tests/polymorphic_universes.v
+++ b/tests/polymorphic_universes.v
@@ -1,5 +1,10 @@
 From HB Require Import structures.
 Set Universe Polymorphism.
-
+Set Printing Universes.
+#[verbose]
 HB.mixin Record isA T := {}.
+
+About isA.phant_axioms.
+
+About isA.axioms_.
 HB.structure Definition A := {T of isA T}.
diff --git a/tests/unit/struct.v b/tests/unit/struct.v
index 6c6a75f4f..1fa97707a 100644
--- a/tests/unit/struct.v
+++ b/tests/unit/struct.v
@@ -1,6 +1,9 @@
 From HB Require Import structures.
+Set Universe Polymorphism.
+Set Printing Universes.
 
 HB.mixin Record m1 T := { default1 : T }.
+Print m1.phant_axioms.
 HB.mixin Record m2 T := { default2 : T }.
 HB.mixin Record is_foo P A := { op : P -> A -> A }.
 HB.structure Definition foo P := { A  of is_foo P A}.

From df7842b2e02c9e0a88cd23e6a0860b2cbb51280c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 24 Sep 2025 10:14:35 +0200
Subject: [PATCH 18/28] make hack

---
 Makefile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Makefile b/Makefile
index a23b34224..f4d8c2de2 100644
--- a/Makefile
+++ b/Makefile
@@ -111,6 +111,7 @@ this-config:: __always__
 	# Remove all of the above when requiring Rocq >= 9.0
 
 this-build:: this-config Makefile.coq
+	cd ../coq-elpi && opam install ./rocq-elpi.opam --ignore-constraints-on=rocq-core
 	+$(COQMAKE)
 
 this-only:: this-config Makefile.coq

From ce2b3d7fb649993948083f4d398752f36812b24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 24 Sep 2025 15:24:12 +0200
Subject: [PATCH 19/28] wip

---
 HB/common/stdpp.elpi |  4 +++-
 HB/common/utils.elpi |  9 +++++----
 HB/instance.elpi     | 20 ++++++++++++--------
 examples/readme.v    | 18 ++++++++++++++++--
 4 files changed, 36 insertions(+), 15 deletions(-)

diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index 4cbbca92c..e40455517 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -303,7 +303,9 @@ cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name.
 % decompose [app (p?global X UI?)|Args] into X and Args, using @univdecl UI to store UI.
 pred coq.safe-dest-global-app i:term, o:gref, o:list term.
 coq.safe-dest-global-app Tm GR Args :- !, std.do![
-    coq.safe-dest-app Tm Head Args, (Head = global GR; Head = pglobal GR _)
+    coq.safe-dest-app Tm Head Args,
+    std.assert! (not(var Head)) "coq.safe-dest-global-app: flexible input term",
+    (Head = global GR; Head = pglobal GR _)
   ].
 
 % ---------------------------------------------------------------------
diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi
index ae4216b66..fd524e453 100644
--- a/HB/common/utils.elpi
+++ b/HB/common/utils.elpi
@@ -49,17 +49,17 @@ argument->gref (str S) GR :- located->gref S {coq.locate-all S} GR.
 argument->gref X _ :- coq.error "Argument" X "is expected to be a string".
 
 pred argument->term i:argument, o:term.
-argument->term (str S) (global GR) :- !, argument->gref (str S) GR.
+argument->term (str S) T :- !, argument->gref (str S) GR, coq.env.global GR T.
 argument->term (trm T) T1 :- !, std.assert-ok! (coq.elaborate-skeleton T _ T1) "not well typed term".
 argument->term X _ :- coq.error "Argument" X " is expected to be a term or a string".
 
 pred argument->ty i:argument, o:term.
-argument->ty (str S) T1 :- !, argument->gref (str S) GR, std.assert-ok! (coq.elaborate-ty-skeleton (global GR) _ T1) "global reference is not a type".
+argument->ty (str S) T1 :- !, argument->gref (str S) GR, coq.env.global GR T, std.assert-ok! (coq.elaborate-ty-skeleton T _ T1) "global reference is not a type".
 argument->ty (trm T) T1 :- !, std.assert-ok! (coq.elaborate-ty-skeleton T _ T1) "not well typed type".
 argument->ty X _ :- coq.error "Argument" X " is expected to be a type or a string".
 
 pred builder->string i:builder, o:string.
-builder->string (builder _ _ _ B) S :- coq.term->string (global B) S.
+builder->string (builder _ _ _ B) S :-  coq.env.global B T, coq.term->string T S.
 
 pred nice-gref->string i:gref, o:string.
 nice-gref->string X Mod :-
@@ -67,7 +67,8 @@ nice-gref->string X Mod :-
   std.rev Path [Mod1,Mod2|_], !,
   Mod is Mod2 ^ "_" ^ Mod1.
 nice-gref->string X S :-
-  coq.term->string (global X) S.
+  coq.env.global X T,
+  coq.term->string T S.
 
 pred gref->modname i:gref, i:int, i:string, o:string.
 gref->modname GR NComp Sep ModName :-
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 1e43b6be6..2ce0c018f 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -26,9 +26,9 @@ pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pai
 declare-const Name BodySkel TyWPSkel CFL CSL :- std.spy-do! [
   std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
   coq.arity->term TyWP Ty,
-  coq.say {coq.term->string Ty},
-  coq.say {coq.term->string BodySkel},
-  std.assert-ok! (coq.elaborate-skeleton BodySkel _ Body) "Definition illtyped WHYYYY?",
+  coq.say "TY=" {coq.term->string Ty},
+  coq.say "BO=" {coq.term->string BodySkel},
+  std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped WHYYYY?",
 
   % handle parameters via a section -- begin
   if (TyWP = arity SectionTy) (
@@ -67,7 +67,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.spy-do! [
     (coq.error "HB: The instance subject must be explicitly given.\nUse:\n  HB.instance Definition _ : M <subject> := ...\n  HB.instance Definition _ := M.Build <subject> ...")
     true,
 
-  std.assert-ok! (coq.typecheck OptimizedBody _) "typechecking Optimized Body",
+  std.assert-ok! (coq.typecheck OptimizedBody SectionTyUnfolded) "typechecking Optimized Body",
   log.coq.env.add-const-noimplicits-failondup RealName OptimizedBody
     SectionTyUnfolded @transparent! C,
   coq.env.global (const C) TheFactory,
@@ -106,11 +106,11 @@ declare-all T [class _ Struct _|Rest] L :- has-instance T Struct, !,
   declare-all T Rest L.
 declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
 
-  infer-class T Class Struct MLwP S Name STy Clauses,
+  std.spy(infer-class T Class Struct MLwP S Name STy Clauses),
 
   !,
 
-  decl-const-in-struct Name S STy CS,
+  std.spy(decl-const-in-struct Name S STy CS),
 
   Clauses => declare-all T Rest L.
 
@@ -178,16 +178,19 @@ infer-class T  Class Struct MLwP S Name STy Clauses:- std.do![
   if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}),
 
   coq.typecheck S STy ok, % failure may be due to a parameter not rich enough see #435
-     
+  
+  if-verbose (coq.say {header} "and it typechecks"),
 ].
 
 pred decl-const-in-struct i:string, i:term, i:term, i:constant.
-decl-const-in-struct Name S STy CS:- std.do![
+decl-const-in-struct Name S STy CS:- std.spy-do![
 
   if (ground_term S) (S1 = S, STy1 = STy)
     (abstract-holes.main S S1,
      std.assert-ok! (coq.typecheck S1 STy1) "HB: structure instance illtyped after generalizing over holes"),
 
+  coq.say "T=" {coq.term->string S1},
+  coq.say "Ty=" {coq.term->string STy1},
   log.coq.env.add-const-noimplicits Name S1 STy1 @transparent! CS, % Bug coq/coq#11155, could be a Let
   with-locality (log.coq.CS.declare-instance CS), % Bug coq/coq#11155, should be local
   acc-clause current (local-canonical CS),
@@ -239,6 +242,7 @@ declare-instance Factory T F Clauses CFL CSL :-
     T F TheFactory FGR Clauses CFL CSL.
 declare-instance Factory T F Clauses CFL CSL :-
   declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
+  coq.say "DONE",
   if (get-option "export" tt)
      (coq.env.current-library File,
       std.map {std.append CFL CSL} (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
diff --git a/examples/readme.v b/examples/readme.v
index e06c107a6..ddf74b6f1 100644
--- a/examples/readme.v
+++ b/examples/readme.v
@@ -46,15 +46,29 @@ Axiom Z_add_comm : forall x y, Z.add x y = Z.add y x.
 Axiom Z_add_0_l : forall x, Z.add Z0 x = x.
 Axiom Z_add_opp_diag_l : forall x, Z.add (Z.opp x) x = Z0.
 
-Fail #[verbose]
+(* Set Debug "backtrace". *)
+
+#[verbose]
 HB.instance Definition Z_CoMoid := AddComoid_of_Type.Build Z Z0 Z.add Z_add_assoc Z_add_comm Z_add_0_l.
+
+
 Section test.
 Universe u u' u''.
+About id_phant.
+About unify.
 Check id_phant@{u+1} : unify@{u+1 max(u'+1,u'')}  Type@{u} Type@{u} Z _
                          (is_not_canonically_a@{max(u'+1,u'')} AddComoid.type@{u' u''}).
+Set Printing All.
+About AbelianGrp_of_AddComoid.phant_Build.
+(* Set Debug "backtrace".
+Set Debug "ustate". *)
+Check Z : AddComoid.type.
+Check AbelianGrp_of_AddComoid.phant_Build Z _ _ (@id_phant _ _) _ (@id_phant _ _) _
+  (@id_phant _ _) _ (@id_phant _ _) (@id_phant _ _) Z.opp Z_add_opp_diag_l.
 
+#[verbose]
 HB.instance Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z_add_opp_diag_l.
-
+stop.
 Lemma example2 (x : Z) : x + (- x) = - 0.
 Proof. by rewrite example. Qed.
 

From 96695c78da447213bbe70b0aadda1f1645ee0011 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 24 Sep 2025 15:52:50 +0200
Subject: [PATCH 20/28] wip

---
 HB/instance.elpi  |  1 +
 examples/readme.v | 10 ++++++----
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/HB/instance.elpi b/HB/instance.elpi
index 2ce0c018f..bd5c60101 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -191,6 +191,7 @@ decl-const-in-struct Name S STy CS:- std.spy-do![
 
   coq.say "T=" {coq.term->string S1},
   coq.say "Ty=" {coq.term->string STy1},
+  coq.univ.print,
   log.coq.env.add-const-noimplicits Name S1 STy1 @transparent! CS, % Bug coq/coq#11155, could be a Let
   with-locality (log.coq.CS.declare-instance CS), % Bug coq/coq#11155, should be local
   acc-clause current (local-canonical CS),
diff --git a/examples/readme.v b/examples/readme.v
index ddf74b6f1..6315e77c5 100644
--- a/examples/readme.v
+++ b/examples/readme.v
@@ -60,11 +60,13 @@ Check id_phant@{u+1} : unify@{u+1 max(u'+1,u'')}  Type@{u} Type@{u} Z _
                          (is_not_canonically_a@{max(u'+1,u'')} AddComoid.type@{u' u''}).
 Set Printing All.
 About AbelianGrp_of_AddComoid.phant_Build.
-(* Set Debug "backtrace".
-Set Debug "ustate". *)
-Check Z : AddComoid.type.
+ Set Debug "backtrace".
+ Set Debug "univMinim".
+ Set Debug "ustate".
+(* Set Debug "ustate". *)
+(* Check Z : AddComoid.type.
 Check AbelianGrp_of_AddComoid.phant_Build Z _ _ (@id_phant _ _) _ (@id_phant _ _) _
-  (@id_phant _ _) _ (@id_phant _ _) (@id_phant _ _) Z.opp Z_add_opp_diag_l.
+  (@id_phant _ _) _ (@id_phant _ _) (@id_phant _ _) Z.opp Z_add_opp_diag_l. *)
 
 #[verbose]
 HB.instance Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z_add_opp_diag_l.

From 07f219a39d6b5cde6594b7de9375848b649ee566 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Wed, 24 Sep 2025 17:15:11 +0200
Subject: [PATCH 21/28] typechecking stuff

---
 HB/factory.elpi   | 4 ++--
 HB/instance.elpi  | 3 ++-
 HB/structure.elpi | 4 ++--
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index 64a2a0fac..02fb9c8c4 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -343,8 +343,8 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
   std.assert-ok! (coq.elaborate-ty-skeleton Ty1Skel _ Ty1) "Illtyped alias factory",
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr Ty1 _) (pr Ty1Closed _) Section,
-  std.assert-ok! (coq.typecheck Ty1Closed _) "Typechecking of Ty1Closed failed",
-  log.coq.env.add-const-noimplicits "axioms_" Ty1Closed _ @transparent! C,
+  std.assert-ok! (coq.typecheck Ty1Closed Ty1ClosedTy) "Typechecking of Ty1Closed failed",
+  log.coq.env.add-const-noimplicits "axioms_" Ty1Closed Ty1ClosedTy @transparent! C,
 
   std.assert! (coq.safe-dest-global-app Ty1 PhF _Args) "Argument must be a factory",
   std.assert-ok! (factory-alias->gref PhF F) "HB",
diff --git a/HB/instance.elpi b/HB/instance.elpi
index bd5c60101..7d2e7c795 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -388,7 +388,8 @@ declare-mixin-name T T [] :- coq.safe-dest-global-app T GR _, not (from _ _ GR),
 declare-mixin-name T G [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}),
-  log.coq.env.add-const-noimplicits Name T _ @transparent! C,
+  std.assert-ok! (coq.typecheck T Ty) "Failing typechecking the mixin",
+  log.coq.env.add-const-noimplicits Name T Ty @transparent! C,
   coq.env.global (const C) G
 ].
 
diff --git a/HB/structure.elpi b/HB/structure.elpi
index f7bd29087..3997ee847 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -64,8 +64,8 @@ declare Module BSkel Sort :- std.do! [
   (ClassAlias => class-def CurrentClass => GRDepsClauses => MixinMems =>
     w-params.then MLwP mk-fun mk-fun (private.pack-body ClassName) Pack),
   if-verbose (coq.say {header} "declaring pack_ constant =" Pack),
-  std.assert-ok! (coq.typecheck Pack _) "typechecking failure: pack_",
-  log.coq.env.add-const-noimplicits "pack_" Pack _ @transparent! ConstPack,
+  std.assert-ok! (coq.typecheck Pack PackTy) "typechecking failure: pack_",
+  log.coq.env.add-const-noimplicits "pack_" Pack PackTy @transparent! ConstPack,
   GRPack = const ConstPack,
 
   if-arg-sort (

From ec8b1ad2e91514431de889ca547d17baa0a1eb12 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Wed, 24 Sep 2025 17:16:24 +0200
Subject: [PATCH 22/28] cleanup

---
 HB/instance.elpi  | 16 +++++++---------
 Makefile          |  1 -
 examples/hulk.v   |  2 +-
 examples/readme.v |  6 ++----
 4 files changed, 10 insertions(+), 15 deletions(-)

diff --git a/HB/instance.elpi b/HB/instance.elpi
index 7d2e7c795..354af491b 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -23,7 +23,7 @@ declare-existing T0 F0 :- std.do! [
 % that can be built using factory instance B. CFL contains the list of
 % factories being defined, CSL the list of canonical structures being defined.
 pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pair id constant).
-declare-const Name BodySkel TyWPSkel CFL CSL :- std.spy-do! [
+declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
   std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
   coq.arity->term TyWP Ty,
   coq.say "TY=" {coq.term->string Ty},
@@ -106,11 +106,11 @@ declare-all T [class _ Struct _|Rest] L :- has-instance T Struct, !,
   declare-all T Rest L.
 declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
 
-  std.spy(infer-class T Class Struct MLwP S Name STy Clauses),
+  infer-class T Class Struct MLwP S Name STy Clauses,
 
   !,
 
-  std.spy(decl-const-in-struct Name S STy CS),
+  decl-const-in-struct Name S STy CS,
 
   Clauses => declare-all T Rest L.
 
@@ -183,15 +183,12 @@ infer-class T  Class Struct MLwP S Name STy Clauses:- std.do![
 ].
 
 pred decl-const-in-struct i:string, i:term, i:term, i:constant.
-decl-const-in-struct Name S STy CS:- std.spy-do![
+decl-const-in-struct Name S STy CS:- std.do![
 
   if (ground_term S) (S1 = S, STy1 = STy)
     (abstract-holes.main S S1,
      std.assert-ok! (coq.typecheck S1 STy1) "HB: structure instance illtyped after generalizing over holes"),
 
-  coq.say "T=" {coq.term->string S1},
-  coq.say "Ty=" {coq.term->string STy1},
-  coq.univ.print,
   log.coq.env.add-const-noimplicits Name S1 STy1 @transparent! CS, % Bug coq/coq#11155, could be a Let
   with-locality (log.coq.CS.declare-instance CS), % Bug coq/coq#11155, should be local
   acc-clause current (local-canonical CS),
@@ -368,12 +365,13 @@ optimize-body (let _ _ T x\x) Red :- !, optimize-body T Red.
 optimize-body X X.
 
 pred hnf i:term, o:term.
-hnf X R :- get-option "hnf" tt, !, unwind {whd X []} R.
+hnf X R :- get-option "hnf" tt, !, whd X [] Y Z, unwind Y Z R.
 hnf X X.
 
 pred optimize-class-body i:term, i:int, i:term, o:term, o:list prop.
 optimize-class-body T NParams (let _ _ MBo R) R1 Clauses :- std.do! [
-  declare-mixin-name {hnf MBo} MC CL1,
+  hnf MBo MBoHNF,
+  declare-mixin-name MBoHNF MC CL1,
   if (coq.env.global (indt _) T, coq.env.global (const C) MC, not(coq.env.opaque? C))
      (log.coq.strategy.set [C] (level 1000)) true, % opaque stops simpl
   optimize-class-body T NParams (R MC) R1 CL2,
diff --git a/Makefile b/Makefile
index f4d8c2de2..a23b34224 100644
--- a/Makefile
+++ b/Makefile
@@ -111,7 +111,6 @@ this-config:: __always__
 	# Remove all of the above when requiring Rocq >= 9.0
 
 this-build:: this-config Makefile.coq
-	cd ../coq-elpi && opam install ./rocq-elpi.opam --ignore-constraints-on=rocq-core
 	+$(COQMAKE)
 
 this-only:: this-config Makefile.coq
diff --git a/examples/hulk.v b/examples/hulk.v
index 9dd523d58..9bce9a238 100644
--- a/examples/hulk.v
+++ b/examples/hulk.v
@@ -1,4 +1,4 @@
-
+Set Universe Polymorphism.
 From HB Require Import structures.
 Require Import ssreflect ssrfun ssrbool.
 
diff --git a/examples/readme.v b/examples/readme.v
index 6315e77c5..9e707e13f 100644
--- a/examples/readme.v
+++ b/examples/readme.v
@@ -60,9 +60,6 @@ Check id_phant@{u+1} : unify@{u+1 max(u'+1,u'')}  Type@{u} Type@{u} Z _
                          (is_not_canonically_a@{max(u'+1,u'')} AddComoid.type@{u' u''}).
 Set Printing All.
 About AbelianGrp_of_AddComoid.phant_Build.
- Set Debug "backtrace".
- Set Debug "univMinim".
- Set Debug "ustate".
 (* Set Debug "ustate". *)
 (* Check Z : AddComoid.type.
 Check AbelianGrp_of_AddComoid.phant_Build Z _ _ (@id_phant _ _) _ (@id_phant _ _) _
@@ -70,7 +67,7 @@ Check AbelianGrp_of_AddComoid.phant_Build Z _ _ (@id_phant _ _) _ (@id_phant _ _
 
 #[verbose]
 HB.instance Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z_add_opp_diag_l.
-stop.
+
 Lemma example2 (x : Z) : x + (- x) = - 0.
 Proof. by rewrite example. Qed.
 
@@ -86,3 +83,4 @@ Goal forall x : T, x + -x = 0.
 Abort.
 
 End Test.
+End test.

From 76ce7d486edc214cdba86e1610a87513b547544f Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Wed, 24 Sep 2025 17:16:46 +0200
Subject: [PATCH 23/28] extra typecheking

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

diff --git a/HB/factory.elpi b/HB/factory.elpi
index 02fb9c8c4..297b63605 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -357,6 +357,7 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
   (pi Args\ copy (app[FHead|Args]) (app[CHead|Section])) => copy MFKTy MFKTyC,
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr MFK MFKTyC) (pr MFKClosed MFKTyCClosed) _,
+  std.assert-ok! (coq.typecheck MFKClosed MFKTyCClosed) "MFKClosed illtyped",
   log.coq.env.add-const-noimplicits "Axioms_" MFKClosed MFKTyCClosed @transparent! CK,
 
   GRK = const CK,

From e44a931533b265e72b3144ef2653a44f391e5091 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Wed, 24 Sep 2025 17:18:27 +0200
Subject: [PATCH 24/28] debug in progress

---
 examples/demo3/hierarchy_1.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/examples/demo3/hierarchy_1.v b/examples/demo3/hierarchy_1.v
index a225c234b..3f1972b4e 100644
--- a/examples/demo3/hierarchy_1.v
+++ b/examples/demo3/hierarchy_1.v
@@ -1,3 +1,4 @@
+Set Universe Polymorphism.
 From Corelib Require Import ssreflect ssrfun.
 From HB Require Import structures.
 
@@ -46,9 +47,9 @@ HB.builders Context A (a : Ring_of_MulMonoid A).
   HB.instance
   Definition to_AddMonoid_of_Type :=
     AddMonoid_of_Type.Build A zero add addrA add0r addr0.
-
-  HB.instance
-  Definition to_Ring_of_AddMulMonoid :=
+  (* Set Debug "backtrace". *)
+  (* Set Debug "ustate". *)
+  Fail #[verbose] HB.instance Definition to_Ring_of_AddMulMonoid :=
     Ring_of_AddMulMonoid.Build A opp addrC addNr mulrDl mulrDr.
 
 HB.end.

From e95aa4f309cc62eae5deb1fd51a91026e0006671 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Wed, 8 Oct 2025 15:38:53 +0200
Subject: [PATCH 25/28] wip

---
 .nix/config.nix              |  4 ++--
 HB/factory.elpi              |  3 +++
 examples/demo3/hierarchy_0.v | 19 ++++++++++++++++++-
 examples/demo3/hierarchy_1.v |  3 ++-
 examples/demo5/hierarchy_0.v |  1 +
 5 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/.nix/config.nix b/.nix/config.nix
index aa96df726..6cf162f59 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -34,14 +34,14 @@
   in {
     "coq-universes-clauses" = {
       rocqPackages = {
-        rocq-core.override.version = "mattam82:universes-clauses";
+        rocq-core.override.version = "CohenCyril:universes-clauses";
         stdlib.override.version = "master";
         rocq-elpi.override.version = "mattam82:universes-clauses";
         rocq-elpi.override.elpi-version = "2.0.7";
         bignums.override.version = "master";
       };
       coqPackages = mcHBcommon // {
-        coq.override.version = "mattam82:universes-clauses";
+        coq.override.version = "CohenCyril:universes-clauses";
         stdlib.override.version = "master";
         coq-elpi.override.version = "mattam82:universes-clauses";
         coq-elpi.override.elpi-version = "2.0.7";
diff --git a/HB/factory.elpi b/HB/factory.elpi
index 297b63605..a2bef86e8 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -267,6 +267,9 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclClosedSkel RDeclClosed) "record declaration illtyped",
 
+  coq.say "RDeclClosed=" RDeclClosed,
+  coq.univ.print,
+
   if (get-option "primitive" tt)
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
     (log.coq.env.add-indt RDeclClosed R),
diff --git a/examples/demo3/hierarchy_0.v b/examples/demo3/hierarchy_0.v
index d0a516834..e73011c7a 100644
--- a/examples/demo3/hierarchy_0.v
+++ b/examples/demo3/hierarchy_0.v
@@ -1,15 +1,32 @@
+Set Printing Universes.
+Set Universe Polymorphism.
 From HB Require Import structures.
 From Corelib Require Import ssreflect ssrfun.
 
-HB.mixin Record MulMonoid_of_Type A := {
+(* Section Toto. *)
+(* Variable A : Type. *)
+(* Universe u. *)
+(* Record MulMonoid_of_Type : Type@{u} := { *)
+(*   one : A; *)
+(*   mul : A -> A -> A; *)
+(*   mulrA : associative mul; *)
+(*   mul1r : left_id one mul; *)
+(*   mulr1 : right_id one mul; *)
+(* }. *)
+(* End Toto. *)
+
+HB.mixin Record MulMonoid_of_Type (A : Type) := {
   one : A;
   mul : A -> A -> A;
   mulrA : associative mul;
   mul1r : left_id one mul;
   mulr1 : right_id one mul;
 }.
+STOP.
+
 HB.structure Definition MulMonoid := { A of MulMonoid_of_Type A }.
 
+
 HB.mixin Record Ring_of_MulMonoid A of MulMonoid A := {
   zero : A;
   add : A -> A -> A;
diff --git a/examples/demo3/hierarchy_1.v b/examples/demo3/hierarchy_1.v
index 3f1972b4e..bbc9175c2 100644
--- a/examples/demo3/hierarchy_1.v
+++ b/examples/demo3/hierarchy_1.v
@@ -1,4 +1,5 @@
 Set Universe Polymorphism.
+Set Printing Universes.
 From Corelib Require Import ssreflect ssrfun.
 From HB Require Import structures.
 
@@ -49,7 +50,7 @@ HB.builders Context A (a : Ring_of_MulMonoid A).
     AddMonoid_of_Type.Build A zero add addrA add0r addr0.
   (* Set Debug "backtrace". *)
   (* Set Debug "ustate". *)
-  Fail #[verbose] HB.instance Definition to_Ring_of_AddMulMonoid :=
+  #[verbose] HB.instance Definition to_Ring_of_AddMulMonoid :=
     Ring_of_AddMulMonoid.Build A opp addrC addNr mulrDl mulrDr.
 
 HB.end.
diff --git a/examples/demo5/hierarchy_0.v b/examples/demo5/hierarchy_0.v
index 8d981f76e..80002f9b5 100644
--- a/examples/demo5/hierarchy_0.v
+++ b/examples/demo5/hierarchy_0.v
@@ -143,6 +143,7 @@ HB.mixin Record LModule_of_AG (R : Ring.type) (M : Type) of AddAG M := {
   scaleA : forall a b v, scale a (scale b v) = scale (a * b) v;
   scale1r : forall m, scale 1 m = m;
 }.
+
 HB.structure Definition LModule (R : Ring.type) :=
   { M of LModule_of_AG R M & }.
 Infix "*:" := (@scale _ _) (at level 30) : hb_scope.

From e550c2b98040f699e8ce84d258d3f11332686bfe Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Wed, 8 Oct 2025 16:18:44 +0200
Subject: [PATCH 26/28] cleanup

---
 examples/demo3/hierarchy_0.v | 1 -
 examples/readme.v            | 3 ---
 2 files changed, 4 deletions(-)

diff --git a/examples/demo3/hierarchy_0.v b/examples/demo3/hierarchy_0.v
index e73011c7a..05f482e5e 100644
--- a/examples/demo3/hierarchy_0.v
+++ b/examples/demo3/hierarchy_0.v
@@ -22,7 +22,6 @@ HB.mixin Record MulMonoid_of_Type (A : Type) := {
   mul1r : left_id one mul;
   mulr1 : right_id one mul;
 }.
-STOP.
 
 HB.structure Definition MulMonoid := { A of MulMonoid_of_Type A }.
 
diff --git a/examples/readme.v b/examples/readme.v
index 9e707e13f..d6baf476a 100644
--- a/examples/readme.v
+++ b/examples/readme.v
@@ -56,9 +56,6 @@ Section test.
 Universe u u' u''.
 About id_phant.
 About unify.
-Check id_phant@{u+1} : unify@{u+1 max(u'+1,u'')}  Type@{u} Type@{u} Z _
-                         (is_not_canonically_a@{max(u'+1,u'')} AddComoid.type@{u' u''}).
-Set Printing All.
 About AbelianGrp_of_AddComoid.phant_Build.
 (* Set Debug "ustate". *)
 (* Check Z : AddComoid.type.

From 80a8600d4c623334b79cc5ee06d5d87cb959cb72 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Wed, 8 Oct 2025 17:06:50 +0200
Subject: [PATCH 27/28] WIP

---
 HB/factory.elpi              | 4 ++--
 HB/instance.elpi             | 4 ++--
 HB/structure.elpi            | 6 +++++-
 examples/demo3/hierarchy_0.v | 4 ++++
 examples/demo5/hierarchy_0.v | 2 +-
 5 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index a2bef86e8..612969c87 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -267,8 +267,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclClosedSkel RDeclClosed) "record declaration illtyped",
 
-  coq.say "RDeclClosed=" RDeclClosed,
-  coq.univ.print,
+  % coq.say "RDeclClosed=" RDeclClosed,
+  % coq.univ.print,
 
   if (get-option "primitive" tt)
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 354af491b..38cc5666b 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -26,8 +26,8 @@ pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pai
 declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
   std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
   coq.arity->term TyWP Ty,
-  coq.say "TY=" {coq.term->string Ty},
-  coq.say "BO=" {coq.term->string BodySkel},
+  % coq.say "TY=" {coq.term->string Ty},
+  % coq.say "BO=" {coq.term->string BodySkel},
   std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped WHYYYY?",
 
   % handle parameters via a section -- begin
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 3997ee847..91c5eb9d1 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -162,6 +162,8 @@ declare Module BSkel Sort :- std.do! [
 
   export.module {calc (Module ^ ".Exports")} Exports,
 
+  coq.say "Struct = " {coq.env.global Structure},
+
   if-verbose (coq.say {header} "exporting operations"),
     ClassAlias => Factories => GRDepsClauses =>
       private.export-operations Structure SortProjection ClassProjection MLwP [] EX MLToExport,
@@ -214,7 +216,7 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
       std.append Params [S|PoArgs] L1,
       std.map L1 copy L2)),
    (pi UI L L1 L2 Params Rest PoArgs\
-    (copy (app [pglobal (const Po) UI | L]) (app [pglobal (const C) UI | L2]) :-
+    (copy (app [pglobal (const Po) UI | L]) (app [pglobal (const C) _ | L2]) :-
       std.split-at NParams L Params [_|Rest],
       std.drop NMixins Rest PoArgs,
       std.append Params [S|PoArgs] L1,
@@ -254,6 +256,8 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std
   w-params.then MwP mk-fun-prod ignore (operation-body-and-ty EXI Poperation Struct Psort Pclass) (pr Body BodyTy),
 
   if-verbose (coq.say {header} "export operation" Name "as" BodyTy),
+  std.assert-ok! (coq.typecheck-ty BodyTy _) "Checking type of operation",
+  std.assert-ok! (coq.typecheck Body BodyTy) "Checking body of operation",
   log.coq.env.add-const-noimplicits Name Body BodyTy @transparent! C,
 
   w-params.nparams MwP NP,
diff --git a/examples/demo3/hierarchy_0.v b/examples/demo3/hierarchy_0.v
index 05f482e5e..45efe02b5 100644
--- a/examples/demo3/hierarchy_0.v
+++ b/examples/demo3/hierarchy_0.v
@@ -38,4 +38,8 @@ HB.mixin Record Ring_of_MulMonoid A of MulMonoid A := {
   mulrDl : left_distributive mul add;
   mulrDr : right_distributive mul add;
 }.
+(* Elpi Trace. *)
+(* Set Debug "backtrace". *)
+(* Set Debug "inferCumul_infer_term". *)
+#[log(raw)]
 HB.structure Definition Ring := { A of MulMonoid A & Ring_of_MulMonoid A }.
diff --git a/examples/demo5/hierarchy_0.v b/examples/demo5/hierarchy_0.v
index 80002f9b5..ad584017b 100644
--- a/examples/demo5/hierarchy_0.v
+++ b/examples/demo5/hierarchy_0.v
@@ -143,7 +143,7 @@ HB.mixin Record LModule_of_AG (R : Ring.type) (M : Type) of AddAG M := {
   scaleA : forall a b v, scale a (scale b v) = scale (a * b) v;
   scale1r : forall m, scale 1 m = m;
 }.
-
+Elpi Trace.
 HB.structure Definition LModule (R : Ring.type) :=
   { M of LModule_of_AG R M & }.
 Infix "*:" := (@scale _ _) (at level 30) : hb_scope.

From fc3f90b28bee00ba074d482dd5f928aae21fa04b Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Thu, 9 Oct 2025 15:55:32 +0200
Subject: [PATCH 28/28] WIP

---
 HB/structure.elpi            | 5 +++--
 HB/structures.v              | 2 +-
 examples/demo5/hierarchy_0.v | 2 --
 tests/interleave_context.v   | 1 +
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/HB/structure.elpi b/HB/structure.elpi
index 91c5eb9d1..3a64af7a1 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -215,8 +215,9 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
       std.drop NMixins Rest PoArgs,
       std.append Params [S|PoArgs] L1,
       std.map L1 copy L2)),
-   (pi UI L L1 L2 Params Rest PoArgs\
-    (copy (app [pglobal (const Po) UI | L]) (app [pglobal (const C) _ | L2]) :-
+   (pi Tm UI L L1 L2 Params Rest PoArgs\
+    (copy (app [pglobal (const Po) UI | L]) (app [Tm | L2]) :-
+      coq.env.global (const C) Tm,
       std.split-at NParams L Params [_|Rest],
       std.drop NMixins Rest PoArgs,
       std.append Params [S|PoArgs] L1,
diff --git a/HB/structures.v b/HB/structures.v
index cd7b152bf..12eca6585 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -652,7 +652,7 @@ Elpi Accumulate File "HB/structure.elpi".
 Elpi Accumulate lp:{{
 
 :name "start"
-main [const-decl N (some B) Arity] :- std.do! [
+main [const-decl N (some B) Arity] :- !, std.do! [
   % compute the universe for the structure (default )
   prod-last {coq.arity->term Arity} Ty,
   if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort,
diff --git a/examples/demo5/hierarchy_0.v b/examples/demo5/hierarchy_0.v
index ad584017b..e46753ff9 100644
--- a/examples/demo5/hierarchy_0.v
+++ b/examples/demo5/hierarchy_0.v
@@ -143,7 +143,6 @@ HB.mixin Record LModule_of_AG (R : Ring.type) (M : Type) of AddAG M := {
   scaleA : forall a b v, scale a (scale b v) = scale (a * b) v;
   scale1r : forall m, scale 1 m = m;
 }.
-Elpi Trace.
 HB.structure Definition LModule (R : Ring.type) :=
   { M of LModule_of_AG R M & }.
 Infix "*:" := (@scale _ _) (at level 30) : hb_scope.
@@ -152,7 +151,6 @@ Definition regular (R : Type) := R.
 
 HB.instance Definition regular_AG (R : AddAG.type) :=
   AddAG_of_TYPE.Build (regular (AddAG.sort R)) zero add opp addrA addrC add0r addNr.
-
 HB.instance Definition regular_LModule (R : Ring.type) :=
   LModule_of_AG.Build R (regular (Ring.sort R)) mul
     (fun _ _ _ => mulrDl _ _ _) mulrDr mulrA mul1r.
diff --git a/tests/interleave_context.v b/tests/interleave_context.v
index 4d615088d..9ab30cc67 100644
--- a/tests/interleave_context.v
+++ b/tests/interleave_context.v
@@ -13,6 +13,7 @@ HB.structure Definition B (X : A.type 0) := { T of HasB X T }.
    parameter `A` to elaborate it. *)
 HB.mixin Record IsSelfA T of A 0 T & B (A.clone 0 T _) T := {}.
 
+(* Elpi Trace. *)
 HB.structure Definition SelfA := { T of IsSelfA T }.
 
 HB.factory Record IsSelfA' T := { a : T ; b : T -> T}.