diff --git a/.nix/config.nix b/.nix/config.nix
index 821e7c49..aa96df72 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/about.elpi b/HB/about.elpi
index 0c2c2806..87d36fbb 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-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"),
@@ -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.
diff --git a/HB/builders.elpi b/HB/builders.elpi
index 4c4ea543..0aa91533 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
+}
diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index 425a8b52..8869e26e 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|_].
diff --git a/HB/common/log.elpi b/HB/common/log.elpi
index 134f9eec..f4f07461 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/common/phant-abbreviation.elpi b/HB/common/phant-abbreviation.elpi
index 943c30c7..cc9b803a 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,
diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index 9264603d..405d4605 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 6444e23c..64e3b3db 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/common/utils.elpi b/HB/common/utils.elpi
index ae4216b6..93c8d203 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/context.elpi b/HB/context.elpi
index 4b04e5f0..3dc2d9b9 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,
diff --git a/HB/factory.elpi b/HB/factory.elpi
index ef00f61a..3443893b 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,
@@ -27,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 = 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! [
+  pdecl->w-mixins Decl (pr MLwP DeclwP),
+  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! [
   if-verbose (coq.say {header} "arguments->w-mixins on const-decl Decl=" CDecl),
@@ -45,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 = 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),
   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.
@@ -213,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
@@ -238,11 +265,16 @@ 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! => 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
@@ -314,15 +346,21 @@ 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! (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 +431,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 +453,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/instance.elpi b/HB/instance.elpi
index 063b4fe0..9e1b08ee 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/pack.elpi b/HB/pack.elpi
index 3bd0d2cc..c18645c3 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",
 
@@ -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-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.
@@ -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.
diff --git a/HB/status.elpi b/HB/status.elpi
index e6bf3684..1913072b 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) :-
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 3702ce19..537b2451 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 (
@@ -87,9 +90,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 +109,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 +141,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 +207,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 +221,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 +289,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 +319,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 +356,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 +379,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 +407,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 +450,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
@@ -454,7 +460,7 @@ 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,
@@ -481,13 +487,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 +523,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 +560,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 +585,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.
diff --git a/HB/structures.v b/HB/structures.v
index 112084d7..79dde2f8 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) :=
@@ -132,7 +133,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".
@@ -487,7 +488,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 +656,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 +695,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 +783,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 +798,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 +854,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 31c827eb..a1100a3c 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/examples/readme.v b/examples/readme.v
index f2a45edd..4009fc2e 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 := {
diff --git a/experiments.v b/experiments.v
new file mode 100644
index 00000000..21bdf95d
--- /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.
diff --git a/tests/polymorphic_universes.v b/tests/polymorphic_universes.v
new file mode 100644
index 00000000..f0e59f2d
--- /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}.