diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index 6ae022a1c..4b66d63bd 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 _ _ X) R :- coq.env.global X R.
 
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
@@ -59,7 +59,8 @@ 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 _ _ B) R :-
+  coq.env.global B R.
 
 pred extract-builder i:prop, o:builder.
 extract-builder (builder-decl B) B.
@@ -114,7 +115,7 @@ 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 :- !,
+extract-conclusion-params TheType T R :- coq.dest-gref-app T GR Args, !,
   factory-alias->gref GR Factory,
   factory-nparams Factory NP,
   std.map Args (copy-pack-holes TheType TheType) NewArgs,
@@ -272,22 +273,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 R :-
   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 R.
 
 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.
@@ -351,7 +353,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, factory-alias->gref GR F, factory-nparams F NP, !,
+  coq.dest-gref-app S GR Args, factory-alias->gref GR F, factory-nparams F NP, !,
   std.split-at NP Args Params [T|_].
 
 % [find-max-classes Mixins Classes] states that Classes is a list of classes
diff --git a/HB/common/log.elpi b/HB/common/log.elpi
index 0e95e073c..4d1b95d9b 100644
--- a/HB/common/log.elpi
+++ b/HB/common/log.elpi
@@ -28,6 +28,14 @@ strategy.set CL S :-
   coq.strategy.set CL S,
   log.private.log-vernac (log.private.coq.vernac.strategy CL S).
 
+pred upoly->flags4const i:prop.
+upoly->flags4const P :- upoly none none, !, P.
+upoly->flags4const P :- @univpoly! => P.
+
+pred upoly->flags4indt i:prop.
+upoly->flags4indt P :- upoly none none, !, P.
+upoly->flags4indt P :- @univpoly-cumul! => P.
+
 pred env.add-const-noimplicits i:id, i:term, i:term, i:opaque?, o:constant.
 env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [
   if (not(ground_term Ty ; ground_term Bo))
@@ -35,7 +43,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,
+  upoly->flags4const (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 +57,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,
+  upoly->flags4const (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 +69,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,
+  upoly->flags4const (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),
@@ -87,7 +95,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,
+  upoly->flags4indt (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 943c30c74..ca701f7cf 100644
--- a/HB/common/phant-abbreviation.elpi
+++ b/HB/common/phant-abbreviation.elpi
@@ -24,7 +24,8 @@ 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,
+  coq.env.global (const C) HD,
+  private.build-abbreviation 0 HD AL NParams AbbrevT,
   @global! => log.coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
 ].
 
@@ -39,7 +40,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 +140,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.dest-gref-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.dest-gref-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 +159,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}},
@@ -200,6 +201,7 @@ 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 (pglobal GR _) :- coq.unify-eq T {{ Type }} ok, !.
 build-type-pattern.aux _ _ _ :- coq.error "HB: wrong carrier type".
 
 
@@ -237,13 +239,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 cd1ffaa4d..3d7b440cc 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -245,3 +245,16 @@ coq.fold-map (primitive _ as C) A C A :- !.
 coq.fold-map (uvar M L as X) A W A1 :- var X, !, std.fold-map L A coq.fold-map L1 A1, coq.mk-app-uvar M L1 W.
 % when used in CHR rules
 coq.fold-map (uvar X L) A (uvar X L1) A1 :- std.fold-map L A coq.fold-map L1 A1.
+
+pred upoly o:option upoly-decl, o:option upoly-decl-cumul.
+
+pred coq.unupoly-argument i:argument, o:argument, o:prop.
+coq.unupoly-argument (upoly-indt-decl I (upoly-decl _ _ _ _ as P))       (indt-decl I) (upoly (some P) none).
+coq.unupoly-argument (upoly-indt-decl I (upoly-decl-cumul _ _ _ _ as P)) (indt-decl I) (upoly none (some P)).
+coq.unupoly-argument (upoly-const-decl N B T P) (const-decl N B T) (upoly (some P) none).
+coq.unupoly-argument X X (upoly none none).
+
+pred coq.dest-gref-app i:term, o:gref, o:list term.
+coq.dest-gref-app T GR Args :-
+  coq.safe-dest-app T HD Args,
+  (HD = global GR ; HD = pglobal GR _).
diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi
index f194be009..a886f56f0 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,
@@ -40,24 +40,29 @@ infer-all-gref-deps Ps T GR X :- std.do! [
 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]) :- !,
   std.map Args (infer-holes-depending-on-pack T) Args1.
+infer-holes-depending-on-params T (app [pglobal GR UI|Args]) (app [pglobal GR UI|Args1]) :- !,
+  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 (pglobal 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 (app[pglobal GR _|_]) Y Z X :- 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 [HD | Args]) S :- coq.env.global GR HD,
   ((coq.gref->id GR GRS, rex.match "phant.*" GRS /*TODO: phant-clone? GR N*/);
     pack? GR _),
+    %% XXX shouldn't we put a bang here?
   coq.env.typeof GR Ty, class-of-phant Ty KC SC C,
   factory-nparams C N,
   std.take N Args Params, !,
   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.
 
@@ -69,7 +74,7 @@ infer-holes-depending-on-pack _ X X.
 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,
 ].
@@ -206,7 +211,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,
@@ -220,7 +225,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.dest-gref-app Tm TmGR _,
   factory-alias->gref TmGR M,
   std.mem! ML M,
   !,
@@ -232,7 +237,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.dest-gref-app Tm TmGR _,
   factory-alias->gref TmGR M,
   if (mixin-for T M X)
      (@pi-def N Tm X m\ instantiate-all-args-let (F m) T (R m) Diag)
@@ -253,18 +258,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,
@@ -276,7 +281,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 ML (m\c\ c = mixin-src T m F) CL.
@@ -287,7 +292,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.dest-gref-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 000826a2a..844054244 100644
--- a/HB/common/utils.elpi
+++ b/HB/common/utils.elpi
@@ -6,6 +6,11 @@
 
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
+pred with-upoly-argument i:argument, i:(argument -> prop).
+with-upoly-argument UArg P :-
+  coq.unupoly-argument UArg Arg Flags,
+  Flags => P Arg.
+
 % HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2
 type attmap attribute-type.
 
@@ -203,7 +208,7 @@ params->holes (w-params.cons _ _ F) [_|PS] :- pi x\ params->holes (F x) PS.
 
 pred fresh-type o:term.
 fresh-type Ty :-
-  Ty = {{Type}},
+  Ty = sort(typ U), coq.univ.new U,
   std.assert-ok! (coq.typecheck-ty Ty _) "impossible".
 
 %%%%%%%%%%%%%%%%%%%%%%
diff --git a/HB/factory.elpi b/HB/factory.elpi
index 2b599df10..12fdb64ff 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -4,10 +4,12 @@
 namespace factory {
 
 pred declare i:argument.
-declare A :- private.declare-asset A private.asset-factory.
+declare A :-
+  with-upoly-argument A (A\ private.declare-asset A private.asset-factory).
 
 pred declare-mixin i:argument.
-declare-mixin A :- private.declare-asset A private.asset-mixin.
+declare-mixin A :-
+  with-upoly-argument A (A\ private.declare-asset A private.asset-mixin).
 
 kind factory-abbrev type.
 type by-classname gref -> factory-abbrev.
@@ -16,7 +18,8 @@ type by-phantabbrev abbreviation -> factory-abbrev.
 pred declare-abbrev i:id, i:factory-abbrev.
 declare-abbrev Name (by-classname GR) :-
   % looks fishy (the parameters are not taken into account)
-  @global! => log.coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt _.
+  coq.env.global GR HD,
+  @global! => log.coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[HD,t]) tt _.
 declare-abbrev Name (by-phantabbrev Abbr) :- std.do! [
   coq.notation.abbreviation-body Abbr Nargs AbbrTrm,
   @global! => log.coq.notation.add-abbreviation Name Nargs AbbrTrm tt _,
@@ -226,11 +229,12 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   if-verbose (coq.say {header} "declare record axioms_"),
   Kname = "Axioms_",
   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 RDeclSkel RDeclClosedSkel _,
 
-  % coq.say RDecl RDeclClosed,
+  std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclClosedSkel RDeclClosed) "record declaration illtyped",
+
+  % coq.say RDeclSkel RDeclClosedSkel RDeclClosed,
 
   if (get-option "primitive" tt)
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
@@ -309,13 +313,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.dest-gref-app Ty1 PhF _Args) "Argument must be a factory",
   std.assert! (factory-alias->gref PhF F) "BUG: Factory alias declaration missing",
   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,
+  (pi Args\ copy (app[global F|Args]) (app[global (const C)|Section])) =>
+  (pi Args UI UI2\ copy (app[pglobal F UI|Args]) (app[pglobal (const C) UI2|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,
@@ -388,7 +394,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,
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 0b793248c..968ea9194 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.dest-gref-app FTy FactoryAlias _)
      "The type of the instance is not a factory",
   factory-alias->gref FactoryAlias Factory,
   private.declare-instance Factory T F Clauses _,
@@ -41,7 +41,7 @@ declare-const Name BodySkel TyWPSkel 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.dest-gref-app SectionTy FactoryAlias Args) "The type of the instance is not a factory",
   factory-alias->gref FactoryAlias Factory,
   std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB",
 
@@ -59,7 +59,7 @@ declare-const Name BodySkel TyWPSkel 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,
 
   % call HB.instance TheType TheFactory
   std.drop NParams Args [TheType|_],
@@ -111,7 +111,7 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
   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}),
   std.assert-ok! (coq.typecheck S STy) "declare-all: S illtyped",
 
@@ -157,7 +157,7 @@ mk-factory-sort-deps AliasGR CSL :- std.do! [
   context.declare MLwPRaw MLwP SortParams SortKey SortMSL _,
   SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort,
   log.coq.env.add-section-variable-noimplicits "f" FSort CF,
-  GCF = global (const CF),
+  coq.env.global (const CF) GCF,
   factory-sort (coercion GRFSort _ GR _),
   SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GRFSort KSort,
   coq.mk-app KSort [GCF] KFSortEta,
@@ -165,7 +165,7 @@ mk-factory-sort-deps AliasGR CSL :- std.do! [
   std.length ML NMLArgs,
   coq.mk-n-holes NMLArgs SortMLHoles,
   std.append {std.append SortParams [SortKey|SortMLHoles]} [GCF] KFSortArgs,
-  coq.mk-app (global GRFSort) KFSortArgs KFSort,
+  coq.mk-app {coq.env.global GRFSort} KFSortArgs KFSort,
   std.assert-ok! (coq.unify-eq KFSortEta KFSort) "HB: KRSort not an app",
   std.map SortMSL
     (c\ o\ sigma m t\ c = mixin-src _ m t, o = mixin-src KFSort m t)
@@ -184,8 +184,8 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [
   log.coq.env.add-section-variable-noimplicits "f" FSort CF,
   std.length {list-w-params_list MLwP} NMLArgs,
   coq.mk-n-holes NMLArgs SortMLHoles,
-  GCF = global (const CF),
-  coq.mk-app (global GR) {std.append SortParams [GCF|SortMLHoles]} FGCF,
+  coq.env.global (const CF) GCF,
+  coq.mk-app {coq.env.global GR} {std.append SortParams [GCF|SortMLHoles]} FGCF,
   declare-const "_" GCF (arity FGCF) CSL
 ].
 
@@ -222,22 +222,22 @@ 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)),
+  MixinSrcCl = mixin-src T MixinName {coq.env.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.dest-gref-app Ty MixinNameAlias _,
   factory-alias->gref MixinNameAlias MixinName,
 
   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 _)) _)
+  if (MakeCanon = tt, whd Bo [] V _, coq.env.global (indc _) V)
      (std.do! [
          if-verbose (coq.say {header} "declare canonical mixin instance" C),
          with-locality (log.coq.CS.declare-instance C),
@@ -265,7 +265,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,
@@ -324,6 +324,10 @@ optimize-body (app[global (const C)| Args]) Red :- (phant-abbrev _ (const C) _ ;
   coq.env.const C (some B) _,
   hd-beta B Args HD Stack,
   unwind HD Stack Red.
+optimize-body (app[pglobal (const C) I| Args]) Red :- (phant-abbrev _ (const C) _ ; (rex_match "phant_" {coq.gref->id (const C)})), !,
+  @uinstance! I => coq.env.const C (some B) _,
+  hd-beta B Args HD Stack,
+  unwind HD Stack Red.
 optimize-body (let _ _ T x\x) Red :- !, optimize-body T Red.
 optimize-body X X.
 
@@ -334,7 +338,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,
@@ -343,19 +347,22 @@ 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 (pglobal _ _ as T) T [].
+declare-mixin-name T G [] :- mixin-mem T GR, coq.env.global GR G.
+declare-mixin-name T T [] :- coq.dest-gref-app T GR _, not (from _ _ GR), not (get-option "hnf" tt).
+declare-mixin-name T GC [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) "mixin instance illtyped",
+  log.coq.env.add-const-noimplicits Name T Ty @transparent! C,
+  coq.env.global (const C) GC,
 ].
 
 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.dest-gref-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 addf308a4..d48032338 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -67,6 +67,7 @@ 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 _) "pack_ illtyped",
   log.coq.env.add-const-noimplicits "pack_" Pack _ @transparent! ConstPack,
   GRPack = const ConstPack,
 
@@ -94,9 +95,9 @@ declare Module BSkel Sort :- std.do! [
       @global! => log.coq.notation.add-abbreviation
         ShortType NStrTypeAbbrev StrTypeTm ff _
     ]) (@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,
@@ -113,8 +114,8 @@ 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))),
-  private.declare-sort-coercion CoeClass Structure SortProjection,
+   (const ArgSortCst)),
+  private.declare-sort-coercion CoeClass Structure {coq.term->gref SortProjection},
 
   if-verbose (coq.say {header} "exporting unification hints"),
   ClassAlias => Factories => GRDepsClauses =>
@@ -145,14 +146,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 _,
 
@@ -231,8 +232,11 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
   w-params.nparams MLwP NParams,
   std.length {list-w-params_list MLwP} NMixins,
 
+  coq.env.global (const Po) GPo,
+  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 [GPo | L]) (app [GC | L2]) :-
       std.split-at NParams L Params [_|Rest],
       std.drop NMixins Rest PoArgs,
       std.append Params [S|PoArgs] L1,
@@ -242,7 +246,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,
@@ -309,13 +313,13 @@ 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\mk-app {coq.env.global x} Params r) BuildersP,
 
-  mk-app (global {get-constructor TC})
+  mk-app {coq.env.global {get-constructor TC}}
     {coq.mk-n-holes {factory-nparams TC}} KCHoles,
 
   (pi c\ sigma Mixes\
@@ -338,12 +342,12 @@ 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,
 
-  mk-app (global {get-constructor StructureT})
+  mk-app {coq.env.global {get-constructor StructureT}}
     {coq.mk-n-holes {factory-nparams TC}} PackPH,
 
   SCoeBody = {{ fun s : lp:StructureP =>
@@ -376,7 +380,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,
@@ -408,9 +412,9 @@ mk-compression-clauses StructureF StructureT [StructureE|Rest] Res :- std.do! [
   std.assert! (coq.coercion.db-for (grefclass StructureF) (grefclass StructureT) [pr C1 Nparams1]) "wrong number of coercions",
   std.assert! (coq.coercion.db-for (grefclass StructureT) (grefclass StructureE) [pr C2 Nparams2]) "wrong number of coercions",
   std.assert! (coq.coercion.db-for (grefclass StructureF) (grefclass StructureE) [pr C3 Nparams3]) "wrong number of coercions",
-  coq.mk-app (global C1) {coq.mk-n-holes Nparams1} F,
-  coq.mk-app (global C2) {coq.mk-n-holes Nparams2} G,
-  coq.mk-app (global C3) {coq.mk-n-holes Nparams3} H,
+  coq.mk-app {coq.env.global C1} {coq.mk-n-holes Nparams1} F,
+  coq.mk-app {coq.env.global C2} {coq.mk-n-holes Nparams2} G,
+  coq.mk-app {coq.env.global C3} {coq.mk-n-holes Nparams3} H,
   RuleSkel = {{ fun x => lp:G (lp:F x) = lp:H x}},
   std.assert-ok! (coq.elaborate-skeleton RuleSkel _ Rule) "coercion composition fails",
   (((pi X L\ coq.fold-map X L X [X|L] :- var X, not(std.exists L (same_var X))) => coq.fold-map Rule [] Rule Holes,
@@ -429,7 +433,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,
@@ -457,7 +461,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.
@@ -503,7 +507,8 @@ mk-record+sort-field Sort _ T F (record RecordName (sort Sort) "Pack" (field _ "
 ].
 
 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 [Class|Args]) _\end-record) :-
+  coq.env.global ClassName Class,
   std.append Params [T] Args.
 
 % Builds the axioms record and the factories from this class to each mixin
@@ -542,13 +547,13 @@ 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) :-
+pred declare-sort-coercion i:class, i:structure, i:gref.
+declare-sort-coercion CoeClass StructureName Proj :-
 
   if-verbose (coq.say {header} "declare sort coercion"),
 
@@ -577,13 +582,13 @@ 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'"),
     MArgs is {factory-nparams NewMixin} + 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 _,
@@ -613,10 +618,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]}
@@ -638,13 +643,13 @@ 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 declare-auto-infer-params-abbrev i:structure, i:mixins, o:located, o:list prop.
 declare-auto-infer-params-abbrev GR MLwP (loc-abbreviation Abbrev) [phant-abbrev GR (const PhC) Abbrev] :-
   get-option "infer" Map, !,
-  Map => mk-infer (global GR) MLwP PhT,
+  Map => mk-infer {coq.env.global GR} MLwP PhT,
   phant.add-abbreviation "type" PhT PhC Abbrev.
 declare-auto-infer-params-abbrev GR _ (loc-gref GR) [].
 
@@ -714,7 +719,7 @@ pred mk-hb-eta.on i:structure, i:term, i:abbreviation,
   i:list term, i:name, i:term, i:A, o:term.
 mk-hb-eta.on Structure SortProjection OnAbbrev
     Params NT _T _ (fun NT Ty Body) :- !, std.do! [
-  coq.mk-app (global Structure) Params Ty,
+  coq.mk-app {coq.env.global Structure} Params Ty,
   @pi-decl NT Ty s\ sigma Tm\ std.do! [
     coq.mk-app {{lib:@hb.eta}}
       [_, {coq.mk-app SortProjection {std.append Params [s]}}]
@@ -728,12 +733,12 @@ pred mk-hb-eta.arity i:structure, i:classname, i:term, i:list term,
   i:name, i:term, i:A, o:arity.
 mk-hb-eta.arity Structure ClassName SortProjection
     Params NT _T _ Out :- !, std.do! [
-  coq.mk-app (global Structure) Params Ty,
+  coq.mk-app {coq.env.global Structure} Params Ty,
   (@pi-decl NT Ty s\ sigma Tm\ std.do! [
     coq.mk-app {{lib:@hb.eta}}
       [_, {coq.mk-app SortProjection {std.append Params [s]}}] Tm,
     std.assert-ok! (coq.typecheck Tm _) "HB: eta illtyped",
-    coq.mk-app (global ClassName) {std.append Params [Tm]} (Concl s)
+    coq.mk-app {coq.env.global ClassName} {std.append Params [Tm]} (Concl s)
   ]),
   Out = parameter {coq.name->id NT} explicit Ty s\ arity (Concl s)
 ].
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
index 98c20167e..0739ae957 100644
--- a/_CoqProject.test-suite
+++ b/_CoqProject.test-suite
@@ -52,6 +52,9 @@ examples/Coq2020_material/CoqWS_abstract.v
 examples/Coq2020_material/CoqWS_expansion/withHB.v
 examples/Coq2020_material/CoqWS_expansion/withoutHB.v
 
+examples/cat/cat.v
+examples/cat/upoly_cat.v
+
 tests/type_of_exported_ops.v
 tests/duplicate_structure.v
 tests/instance_params_no_type.v
diff --git a/examples/cat/upoly_cat.v b/examples/cat/upoly_cat.v
new file mode 100644
index 000000000..a8a8c38fb
--- /dev/null
+++ b/examples/cat/upoly_cat.v
@@ -0,0 +1,646 @@
+Require Import ssreflect ssrfun.
+From HB Require Import structures.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Add Search Blacklist "__canonical__".
+Set Universe Polymorphism.
+
+Declare Scope cat_scope.
+Delimit Scope cat_scope with cat.
+Local Open Scope cat_scope.
+
+Axiom funext : forall {T : Type} {U : T -> Type} [f g : forall t, U t],
+  (forall t, f t = g t) -> f = g.
+Axiom propext : forall P Q : Prop, P <-> Q -> P = Q.
+Axiom Prop_irrelevance : forall (P : Prop) (x y : P), x = y.
+
+Definition U := Type.
+Identity Coercion U_to_type : U >-> Sortclass.
+
+HB.mixin Record HasHom C := { hom : C -> C -> U }.
+
+About HasHom.axioms_.
+
+#[verbose] HB.structure Definition Hom : Set := { C of HasHom C }.
+
+Notation homType := Hom.type.
+Bind Scope cat_scope with Hom.type.
+Bind Scope cat_scope with hom.
+Arguments hom {C} : rename.
+Notation "a ~> b" := (hom a b)
+   (at level 99, b at level 200, format "a  ~>  b") : cat_scope.
+
+HB.mixin Record Hom_IsPreCat C of Hom C := {
+  idmap : forall (a : C), a ~> a;
+  comp : forall (a b c : C), (a ~> b) -> (b ~> c) -> (a ~> c);
+}.
+
+HB.factory Record IsPreCat C := {
+  hom : C -> C -> U;
+  idmap : forall (a : C), hom a a;
+  comp : forall (a b c : C), hom a b -> hom b c -> hom a c;
+}.
+HB.builders Context C of IsPreCat C.
+  HB.instance Definition _ := HasHom.Build C hom.
+  HB.instance Definition _ := Hom_IsPreCat.Build C idmap comp.
+HB.end.
+
+Un
+
+HB.structure Definition PreCat : Set := { C of IsPreCat C }.
+
+
+Notation precat := PreCat.type.
+Bind Scope cat_scope with precat.
+Arguments idmap {C} {a} : rename.
+Arguments comp {C} {a b c} : rename.
+
+Notation "f \o g" := (comp g f) : cat_scope.
+Notation "f \; g" := (comp f g) : cat_scope.
+Notation "\idmap_ a" := (@idmap _ a) (only parsing, at level 0) : cat_scope.
+
+HB.mixin Record PreCat_IsCat C of PreCat C := {
+  comp1o : forall (a b : C) (f : a ~> b), idmap \; f = f;
+  compo1 : forall (a b : C) (f : a ~> b), f \; idmap = f;
+  compoA : forall (a b c d : C) (f : a ~> b) (g : b ~> c) (h : c ~> d),
+    f \; (g \; h) = (f \; g) \; h
+}.
+Un
+
+HB.structure Definition Cat : Set := { C of PreCat_IsCat C & IsPreCat C }.
+
+
+Notation cat := Cat.type.
+Arguments compo1 {C a b} : rename.
+Arguments comp1o {C a b} : rename.
+Arguments compoA {C a b c d} : rename.
+
+Definition discrete (T : Type) := T.
+HB.instance Definition _ T := @IsPreCat.Build (discrete T) (fun x y => x = y)
+  (fun=> erefl) (@etrans _).
+Lemma etransA T (a b c d : discrete T) (f : a ~> b) (g : b ~> c) (h : c ~> d) :
+    f \; (g \; h) = (f \; g) \; h.
+Proof. by rewrite /idmap/comp/=; case: _ / h; case: _ / g. Qed.
+HB.instance Definition _ T := PreCat_IsCat.Build (discrete T) (@etrans_id _)
+   (fun _ _ _ => erefl) (@etransA _).
+
+HB.instance Definition _ := Cat.copy unit (discrete unit).
+
+HB.instance Definition _ := @IsPreCat.Build U (fun A B => A -> B)
+  (fun a => idfun) (fun a b c (f : a -> b) (g : b -> c) => (g \o f)%FUN).
+HB.instance Definition _ := PreCat_IsCat.Build U (fun _ _ _ => erefl)
+  (fun _ _ _ => erefl) (fun _ _ _ _ _ _ _ => erefl).
+
+Lemma Ucomp (X Y Z : U) (f : X ~> Y) (g : Y ~> Z) : f \; g = (g \o f)%FUN.
+Proof. by []. Qed.
+Lemma Ucompx (X Y Z : U) (f : X ~> Y) (g : Y ~> Z) x : (f \; g) x = g (f x).
+Proof. by []. Qed.
+Lemma U1 (X : U) : \idmap_X = idfun.
+Proof. by []. Qed.
+Lemma U1x (X : U) x : \idmap_X x = x.
+Proof. by []. Qed.
+
+HB.mixin Record IsPreFunctor (C D : Hom.type) (F : C -> D) := {
+   Fhom_of : forall (a b : C), (a ~> b) -> (F a ~> F b)
+}.
+
+Un
+
+HB.structure Definition PreFunctor (C D : Hom.type) : Set :=
+  { F of IsPreFunctor C D F }.
+
+
+HB.instance Definition _ := HasHom.Build Hom.type PreFunctor.type.
+Arguments Fhom_of /.
+
+Definition Fhom_phant (C D : Hom.type) (F : C ~> D)
+  of phantom (_ -> _) F := @Fhom_of C D F.
+Notation "F ^$" := (@Fhom_phant _ _ _ (Phantom (_ -> _) F) _ _)
+   (at level 1, format "F ^$") : cat_scope.
+Notation "F <$> f" := (@Fhom_phant _ _ _ (Phantom (_ -> _) F) _ _ f)
+   (at level 58, format "F  <$>  f", right associativity) : cat_scope.
+
+Lemma prefunctorP (C D : homType) (F G : C ~> D) (eqFG : F =1 G) :
+   let homF a b F := F a ~> F b in
+   (forall a b f, eq_rect _ (homF a b) (F <$> f) _ (funext eqFG) = G <$> f) ->
+  F = G.
+Proof.
+rewrite !/Fhom_phant/=.
+move: F G => [F [[/= Fhom]]] [G [[/= Ghom]]] in eqFG *.
+case: _ / (funext eqFG) => /= in Ghom * => eqFGhom.
+congr PreFunctor.Pack; congr PreFunctor.Class; congr IsPreFunctor.Axioms_.
+by do 3!apply: funext=> ?.
+Qed.
+
+HB.mixin Record PreFunctor_IsFunctor (C D : precat) (F : C -> D)
+     of @PreFunctor C D F := {
+   F1 : forall (a : C), F^$ \idmap_a = \idmap_(F a);
+   Fcomp : forall (a b c : C) (f : a ~> b) (g : b ~> c),
+      F^$ (f \; g) = F^$ f \; F^$ g;
+}.
+Un
+
+HB.structure Definition Functor (C D : precat) : Set :=
+  { F of IsPreFunctor C D F & PreFunctor_IsFunctor C D F }.
+
+
+HB.instance Definition _ := HasHom.Build precat Functor.type.
+HB.instance Definition _ := HasHom.Build cat Functor.type.
+
+Lemma functorP (C D : precat) (F G : C ~> D) (eqFG : F =1 G) :
+   let homF a b F := F a ~> F b in
+   (forall a b f, eq_rect _ (homF a b) (F^$ f) _ (funext eqFG) = G^$ f) ->
+  F = G.
+Proof.
+move=> /= /prefunctorP {eqFG}.
+case: F G => [F [/= Fm Fm']] [G [/= Gm Gm']]//=.
+move=> [_] /EqdepFacts.eq_sigT_iff_eq_dep eqFG.
+case: _ / eqFG in Gm' *.
+congr Functor.Pack; congr Functor.Class.
+case: Fm' Gm' => [F1 Fc] [G1 Gc].
+by congr PreFunctor_IsFunctor.Axioms_; apply: Prop_irrelevance.
+Qed.
+
+HB.instance Definition _ (C : precat) :=
+  IsPreFunctor.Build C C idfun (fun a b => idfun).
+HB.instance Definition _ (C : precat) :=
+  PreFunctor_IsFunctor.Build C C idfun (fun=> erefl) (fun _ _ _ _ _ => erefl).
+
+Section comp_prefunctor.
+Context {C D E : homType} {F : C ~> D} {G : D ~> E}.
+
+HB.instance Definition _ := IsPreFunctor.Build C E (G \o F)%FUN
+   (fun a b f => G^$ (F^$ f)).
+Lemma comp_Fun (a b : C) (f : a ~> b) : (G \o F)%FUN^$ f = G^$ (F^$ f).
+Proof. by []. Qed.
+End comp_prefunctor.
+
+Section comp_functor.
+Context {C D E : precat} {F : C ~> D} {G : D ~> E}.
+Lemma comp_F1 (a : C) : (G \o F)%FUN^$ \idmap_a = \idmap_((G \o F)%FUN a).
+Proof. by rewrite !comp_Fun !F1. Qed.
+Lemma comp_Fcomp  (a b c : C) (f : a ~> b) (g : b ~> c) :
+  (G \o F)%FUN^$ (f \; g) = (G \o F)%FUN^$ f \; (G \o F)%FUN^$ g.
+Proof. by rewrite !comp_Fun !Fcomp. Qed.
+HB.instance Definition _ := PreFunctor_IsFunctor.Build C E (G \o F)%FUN
+   comp_F1 comp_Fcomp.
+End comp_functor.
+
+HB.instance Definition _ := Hom_IsPreCat.Build precat
+  (fun C => [the C ~> C of idfun])
+  (fun C D E (F : C ~> D) (G : D ~> E) => [the C ~> E of (G \o F)%FUN]).
+HB.instance Definition _ := Hom_IsPreCat.Build cat
+  (fun C => [the C ~> C of idfun])
+  (fun C D E (F : C ~> D) (G : D ~> E) => [the C ~> E of (G \o F)%FUN]).
+
+Lemma funext_frefl A B (f : A -> B) : funext (frefl f) = erefl.
+Proof. exact: Prop_irrelevance. Qed.
+
+Definition precat_cat : PreCat_IsCat precat.
+Proof.
+by split=> [C D F|C D F|C D C' D' F G H];
+   apply/functorP => a b f /=; rewrite funext_frefl.
+Qed.
+HB.instance Definition _ := precat_cat.
+Definition cat_cat : PreCat_IsCat cat.
+Proof.
+by split=> [C D F|C D F|C D C' D' F G H];
+   apply/functorP => a b f /=; rewrite funext_frefl.
+Qed.
+HB.instance Definition _ := cat_cat.
+
+HB.mixin Record Hom_IsPreConcrete T of Hom T := {
+  concrete : T -> U;
+  concrete_fun : forall (a b : T), (a ~> b) -> (concrete a) -> (concrete b);
+}.
+Un
+
+HB.structure Definition PreConcreteHom : Set :=
+  { C of Hom_IsPreConcrete C & HasHom C }.
+
+
+Coercion concrete : PreConcreteHom.sort >-> U.
+
+HB.mixin Record PreConcrete_IsConcrete T of PreConcreteHom T := {
+  concrete_fun_inj : forall (a b : T), injective (concrete_fun a b)
+}.
+Un
+
+HB.structure Definition ConcreteHom : Set :=
+  { C of PreConcreteHom C & PreConcrete_IsConcrete C }.
+
+
+
+HB.instance Definition _ (C : ConcreteHom.type) :=
+  IsPreFunctor.Build _ _ (concrete : C -> U) concrete_fun.
+
+HB.mixin Record PreCat_IsConcrete T of ConcreteHom T & PreCat T := {
+  concrete1 : forall (a : T), concrete <$> \idmap_a = idfun;
+  concrete_comp : forall (a b c : T) (f : a ~> b) (g : b ~> c),
+    concrete <$> (f \; g) = ((concrete <$> g) \o (concrete <$> f))%FUN;
+}.
+Un
+
+HB.structure Definition ConcretePreCat : Set :=
+  { C of PreCat C & ConcreteHom C & PreCat_IsConcrete C }.
+HB.structure Definition ConcreteCat : Set :=
+  { C of Cat C & ConcreteHom C & PreCat_IsConcrete C }.
+
+
+
+HB.instance Definition _ (C : ConcretePreCat.type) :=
+  PreFunctor_IsFunctor.Build _ _ (concrete : C -> U) (@concrete1 _) (@concrete_comp _).
+HB.instance Definition _ (C : ConcreteCat.type) :=
+  PreFunctor_IsFunctor.Build _ _ (concrete : C -> U) (@concrete1 _) (@concrete_comp _).
+
+HB.instance Definition _ := Hom_IsPreConcrete.Build U (fun _ _ => id).
+HB.instance Definition _ := PreConcrete_IsConcrete.Build U (fun _ _ _ _ => id).
+HB.instance Definition _ := PreCat_IsConcrete.Build U
+   (fun=> erefl) (fun _ _ _ _ _ => erefl).
+
+Un
+
+HB.instance Definition _ := Hom_IsPreConcrete.Build homType (fun _ _ => id).
+HB.instance Definition _ := Hom_IsPreConcrete.Build precat (fun _ _ => id).
+HB.instance Definition _ := Hom_IsPreConcrete.Build cat (fun _ _ => id).
+Lemma homType_concrete_subproof : PreConcrete_IsConcrete homType.
+Proof.
+constructor=> C D F G FG; apply: prefunctorP.
+  by move=> x; congr (_ x); apply: FG.
+by move=> *; apply: Prop_irrelevance.
+Qed.
+HB.instance Definition _ := homType_concrete_subproof.
+
+Lemma precat_concrete_subproof : PreConcrete_IsConcrete precat.
+Proof.
+constructor=> C D F G FG; apply: functorP.
+  by move=> x; congr (_ x); apply: FG.
+by move=> *; apply: Prop_irrelevance.
+Qed.
+HB.instance Definition _ := precat_concrete_subproof.
+
+Lemma cat_concrete_subproof : PreConcrete_IsConcrete cat.
+Proof.
+constructor=> C D F G FG; apply: functorP.
+  by move=> x; congr (_ x); apply: FG.
+by move=> *; apply: Prop_irrelevance.
+Qed.
+HB.instance Definition _ := cat_concrete_subproof.
+HB.instance Definition _ := PreCat_IsConcrete.Build precat
+   (fun=> erefl) (fun _ _ _ _ _ => erefl).
+HB.instance Definition _ := PreCat_IsConcrete.Build cat
+   (fun=> erefl) (fun _ _ _ _ _ => erefl).
+
+
+
+Definition cst (C D : homType) (c : C) := fun of D => c.
+Arguments cst {C} D c.
+HB.instance Definition _ {C D : precat} (c : C) :=
+  IsPreFunctor.Build D C (cst D c) (fun _ _ _ => idmap).
+HB.instance Definition _ {C D : cat} (c : C) :=
+  PreFunctor_IsFunctor.Build D C (cst D c) (fun=> erefl)
+    (fun _ _ _ _ _ => esym (compo1 idmap)).
+
+Definition catop (C : Type) : Type := C.
+HB.instance Definition _ (C : homType) := HasHom.Build (catop C) (fun a b => hom b a).
+HB.instance Definition _ (C : precat) := Hom_IsPreCat.Build (catop C) (fun=> idmap)
+   (fun _ _ _ f g => g \; f).
+HB.instance Definition _ (C : cat) := PreCat_IsCat.Build (catop C)
+   (fun _ _ _ => compo1 _) (fun _ _ _ => comp1o _)
+   (fun _ _ _ _ _ _ _ => esym (compoA _ _ _)).
+Notation "C ^op" := (catop C) (at level 10, format "C ^op") : cat_scope.
+
+
+HB.instance Definition _ {C : precat} {c : C} :=
+  IsPreFunctor.Build C _ (hom c) (fun a b f g => g \; f).
+Lemma hom_Fhom_subproof (C : cat) (x : C) :
+  PreFunctor_IsFunctor _ _ (hom x).
+Proof. by split=> *; apply/funext => h; [apply: compo1 | apply: compoA]. Qed.
+HB.instance Definition _ {C : cat} {c : C} := hom_Fhom_subproof c.
+
+Lemma hom_op {C : homType} (c : C^op) : hom c = (@hom C)^~ c.
+Proof. reflexivity. Qed.
+
+Lemma homFhomx {C : precat} (a b c : C) (f : a ~> b) (g : c ~> a) :
+  (hom c <$> f) g = g \; f.
+Proof. by []. Qed.
+
+Notation "C ~> D :> T" := ([the T of C] ~> [the T of D])
+  (at level 99, D, T at level 200, format "C  ~>  D  :>  T").
+Notation "C :~>: D :> T" := ([the T of C : Type] ~> [the T of D : Type])
+  (at level 99, D, T at level 200, format "C  :~>:  D  :>  T").
+
+Definition dprod {I : Type} (C : I -> Type) := forall i, C i.
+
+Section hom_dprod.
+Context {I : Type} (C : I -> Hom.type).
+Definition dprod_hom_subdef (a b : dprod C) := forall i, a i ~> b i.
+HB.instance Definition _ := HasHom.Build (dprod C) dprod_hom_subdef.
+End hom_dprod.
+Arguments dprod_hom_subdef /.
+
+Section precat_dprod.
+Context {I : Type} (C : I -> precat).
+Definition dprod_idmap_subdef (a : dprod C) : a ~> a := fun=> idmap.
+Definition dprod_comp_subdef (a b c : dprod C) (f : a ~> b) (g : b ~> c) : a ~> c :=
+  fun i => f i \; g i.
+HB.instance Definition _ := IsPreCat.Build (dprod C)
+   dprod_idmap_subdef dprod_comp_subdef.
+End precat_dprod.
+Arguments dprod_idmap_subdef /.
+Arguments dprod_comp_subdef /.
+
+Section cat_dprod.
+Context {I : Type} (C : I -> cat).
+Local Notation type := (dprod C).
+Lemma dprod_is_cat : PreCat_IsCat type.
+Proof.
+split=> [a b f|a b f|a b c d f g h]; apply/funext => i;
+[exact: comp1o | exact: compo1 | exact: compoA].
+Qed.
+HB.instance Definition _ := dprod_is_cat.
+End cat_dprod.
+
+Section hom_prod.
+Context {C D : Hom.type}.
+Definition prod_hom_subdef (a b : C * D) := ((a.1 ~> b.1) * (a.2 ~> b.2))%type.
+HB.instance Definition _ := HasHom.Build (C * D)%type prod_hom_subdef.
+End hom_prod.
+
+Section precat_prod.
+Context {C D : precat}.
+HB.instance Definition _ := IsPreCat.Build (C * D)%type (fun _ => (idmap, idmap))
+  (fun a b c (f : a ~> b) (g : b ~> c) => (f.1 \; g.1, f.2 \; g.2)).
+End precat_prod.
+
+Section cat_prod.
+Context {C D : cat}.
+Local Notation type := (C * D)%type.
+Lemma prod_is_cat : PreCat_IsCat type.
+Proof.
+split=> [[a1 a2] [b1 b2] [f1 f2]|[a1 a2] [b1 b2] [f1 f2]|
+  [a1 a2] [b1 b2] [c1 c2] [d1 d2] [f1 f2] [g1 g2] [h1 h2]]; congr (_, _) => //=;
+by [exact: comp1o | exact: compo1 | exact: compoA].
+Qed.
+HB.instance Definition _ := prod_is_cat.
+End cat_prod.
+
+HB.mixin Record IsNatural (C D : precat) (F G : C :~>: D :> homType)
+     (n : forall c, F c ~> G c) := {
+   natural : forall (a b : C) (f : a ~> b), F <$> f \; n b = n a \; G <$> f
+}.
+Un
+
+HB.structure Definition Natural (C D : precat)
+    (F G : C :~>: D :> homType) : Set :=
+  { n of @IsNatural C D F G n }.
+
+
+HB.instance Definition _  (C D : precat) :=
+  HasHom.Build (PreFunctor.type C D) (@Natural.type C D).
+HB.instance Definition _  (C D : precat) :=
+  HasHom.Build (Functor.type C D) (@Natural.type C D).
+Arguments natural {C D F G} n [a b] f : rename.
+
+Lemma naturalx (C : precat) (D : ConcretePreCat.type)
+  (F G : C :~>: D :> homType) (n : F ~> G)  (a b : C) (f : a ~> b) g :
+    (concrete <$> n b) ((concrete <$> F <$> f) g) =
+    (concrete <$> G <$> f) ((concrete <$> n a) g).
+Proof.
+have /(congr1 (fun h  => (concrete <$> h) g)) := natural n f.
+by rewrite !Fcomp.
+Qed.
+Arguments naturalx {C D F G} n [a b] f.
+
+Lemma naturalU (C : precat) (F G : C :~>: U :> homType) (n : F ~> G)
+   (a b : C) (f : a ~> b) g :  n b (F^$ f g) = G^$ f (n a g).
+Proof. exact: (naturalx n). Qed.
+
+Lemma natP (C D : precat) (F G : C :~>: D :> homType) (n m : F ~> G) :
+  Natural.sort n = Natural.sort m -> n = m.
+Proof.
+case: n m => [/= n nP] [/= m mP] enm.
+elim: _ / enm in mP *; congr Natural.Pack.
+case: nP mP => [[?]] [[?]]; congr Natural.Class.
+congr IsNatural.Axioms_.
+exact: Prop_irrelevance.
+Qed.
+
+Notation "F ~~> G" :=
+   ((F : _ -> _) ~> (G : _ -> _) :> (_ :~>: _ :> homType))
+  (at level 99, G at level 200, format "F  ~~>  G").
+Notation "F ~~> G :> C ~> D" :=
+   ((F : _ -> _) ~> (G : _ -> _) :> (C :~>: D :> homType))
+  (at level 99, G at level 200, C, D at level 0, format "F  ~~>  G  :>  C  ~>  D").
+
+Section hom_repr.
+Context {C : cat} (F : C ~> U :> cat).
+
+Definition homF (c : C) : U := hom c ~~> F.
+
+Section nat.
+Context (x y : C) (xy : x ~> y) (n : hom x ~~> F).
+Definition homFhom_subdef c : hom y c ~> F c := fun g => n _ (xy \; g).
+Arguments homFhom_subdef / : clear implicits.
+
+Lemma homFhom_natural_subdef : IsNatural _ _ _ _ homFhom_subdef.
+Proof.
+by split=> a b f /=; apply/funext => g /=; rewrite !Ucompx/= !naturalU/= Fcomp.
+Qed.
+HB.instance Definition _ := homFhom_natural_subdef.
+Definition homFhom_subdef_nat : hom y ~~> F := [the _ ~~> _ of homFhom_subdef].
+End nat.
+Arguments homFhom_subdef / : clear implicits.
+
+
+HB.instance Definition _ := IsPreFunctor.Build _ _ homF homFhom_subdef_nat.
+Lemma homF_functor_subproof : PreFunctor_IsFunctor _ _ homF.
+Proof.
+split=> [a|a b c f g].
+  apply/funext => -[/= f natf].
+  apply: natP => //=; apply: funext => b; apply: funext => g/=.
+  by rewrite comp1o.
+apply/funext => -[/= h natf].
+apply: natP => //=; apply: funext => d; apply: funext => k/=.
+by rewrite compoA.
+Qed.
+HB.instance Definition _ := homF_functor_subproof.
+
+Section pointed.
+Context (c : C).
+Definition hom_repr : homF c ~> F c := fun f => f _ idmap.
+Arguments hom_repr /.
+
+Definition repr_hom (fc : F c) a :
+   [the C :~>: U :> homType of hom c] a ~> F a := fun f => F^$ f fc.
+Arguments repr_hom / : clear implicits.
+Lemma repr_hom_subdef (fc : F c) : IsNatural _ _ _ _ (repr_hom fc).
+Proof. by split=> a b f /=; apply/funext=> x; rewrite !Ucompx/= Fcomp. Qed.
+HB.instance Definition _ {fc : F c} := repr_hom_subdef fc.
+
+Definition repr_hom_nat : F c ~> homF c := fun fc =>
+   [the hom c ~~> F of repr_hom fc].
+
+Lemma hom_reprK : cancel hom_repr repr_hom_nat.
+Proof.
+move=> f; apply/natP; apply/funext => a; apply/funext => g /=.
+by rewrite -naturalU/=; congr (f _ _); apply: comp1o.
+Qed.
+Lemma repr_homK : cancel repr_hom_nat hom_repr.
+Proof. by move=> fc; rewrite /= F1. Qed.
+End pointed.
+Arguments hom_repr /.
+Arguments repr_hom /.
+
+Lemma hom_repr_natural_subproof : IsNatural _ _ _ _ hom_repr.
+Proof.
+split=> a b f /=; apply/funext => n /=; rewrite !Ucompx/= compo1/=.
+by rewrite -naturalU/=; congr (n _ _); apply/esym/comp1o.
+Qed.
+
+HB.instance Definition _ := hom_repr_natural_subproof.
+Lemma hom_natural_repr_subproof : IsNatural _ _ _ _ repr_hom_nat.
+Proof.
+split=> a b f /=; apply: funext => fa /=; rewrite !Ucompx/=.
+apply: natP; apply: funext => c /=; apply: funext => d /=.
+by rewrite Fcomp Ucompx/=.
+Qed.
+HB.instance Definition _ := hom_natural_repr_subproof.
+
+Definition hom_repr_nat := [the homF ~~> F of hom_repr].
+Definition repr_hom_nat_nat := [the F ~~> homF of repr_hom_nat].
+
+End hom_repr.
+
+Module comma.
+Section homcomma.
+Context {C D E : precat} (F : C ~> E) (G : D ~> E).
+
+Definition type := { x : C * D & F x.1 ~> G x.2 }.
+Definition hom_subdef (a b : type) := {
+    f : tag a ~> tag b & F^$ f.1 \; tagged b = tagged a \; G^$ f.2
+  }.
+HB.instance Definition _ := HasHom.Build type hom_subdef.
+End homcomma.
+Arguments hom_subdef /.
+Section comma.
+Context {C D E : cat} (F : C ~> E) (G : D ~> E).
+Notation type := (type F G).
+
+Program Definition idmap_subdef (a : type) : a ~> a := @Tagged _ idmap _ _.
+Next Obligation. by rewrite !F1 comp1o compo1. Qed.
+Program Definition comp_subdef (a b c : type) (f : a ~> b) (g : b ~> c) : a ~> c :=
+  @Tagged _ (tag f \; tag g) _ _.
+Next Obligation. by rewrite !Fcomp -compoA (tagged g) compoA (tagged f) compoA. Qed.
+HB.instance Definition _ := IsPreCat.Build type idmap_subdef comp_subdef.
+Arguments idmap_subdef /.
+Arguments comp_subdef /.
+
+Lemma comma_homeqP (a b : type) (f g : a ~> b) : projT1 f = projT1 g -> f = g.
+Proof.
+case: f g => [f fP] [g +]/= eqfg; case: _ / eqfg => gP.
+by congr existT; apply: Prop_irrelevance.
+Qed.
+
+Lemma comma_is_cat : PreCat_IsCat type.
+Proof.
+by split=> [[a fa] [b fb] [*]|[a fa] [b fb] [*]|*];
+   apply/comma_homeqP; rewrite /= ?(comp1o, compo1, compoA).
+Qed.
+HB.instance Definition _ := comma_is_cat.
+End comma.
+End comma.
+Notation "F `/` G" := (@comma.type _ _ _ F G)
+  (at level 40, G at level 40, format "F `/` G") : cat_scope.
+Notation "a /` G" := (cst unit a `/` G)
+  (at level 40, G at level 40, format "a /` G") : cat_scope.
+Notation "F `/ b" := (F `/` cst unit b)
+  (at level 40, b at level 40, format "F `/ b") : cat_scope.
+Notation "a / b" := (cst unit a `/ b) : cat_scope.
+
+HB.mixin Record PreCat_IsMonoidal C of PreCat C := {
+  one : C;
+  prod : (C * C)%type ~> C :> precat ;
+}.
+HB.structure Definition PreMonoidal := { C of PreCat C & PreCat_IsMonoidal C }.
+Notation premonoidal := PreMonoidal.type.
+Arguments prod {C} : rename.
+Notation "a * b" := (prod (a, b)) : cat_scope.
+Reserved Notation "f ** g"   (at level 40, g at level 40, format "f  **  g").
+Notation "f ** g" := (prod^$ (f, g)) (only printing) : cat_scope.
+Notation "f ** g" := (prod^$ ((f, g) : (_, _) ~> (_, _))) (only parsing) : cat_scope.
+Notation "1" := one.
+
+Definition hom_cast {C : homType} {a a' : C} (eqa : a = a') {b b' : C} (eqb : b = b') :
+  (a ~> b) -> (a' ~> b').
+Proof. now elim: _ / eqa; elim: _ / eqb. Defined.
+
+
+HB.mixin Record PreFunctor_IsMonoidal (C D : premonoidal) F of @PreFunctor C D F := {
+  fun_one : F 1 = 1;
+  fun_prod : forall (x y : C), F (x * y) = F x * F y;
+  (* fun_prodF : forall (x x' : C) (f : x ~> x') (y y' : C) (g : y ~> y'), *)
+  (*   hom_cast (fun_prod _ _) (fun_prod _ _) (F^$ (f ** g)) = F^$ f ** F^$ g *)
+}.
+HB.structure Definition MonoidalPreFunctor C D := { F of @PreFunctor_IsMonoidal C D F }.
+Arguments fun_prod {C D F x y} : rename.
+(* Arguments fun_prodF {C D F x x'} f {y y'} g : rename. *)
+Un
+
+HB.instance Definition _ := HasHom.Build premonoidal MonoidalPreFunctor.type.
+
+
+
+(* Definition comma_is_premonoidal (C D E : premonoidal) *)
+(*   (F : C ~> E) (G : D ~> E) := F. *)
+
+HB.instance Definition _ (C : Hom.type) :=
+  IsPreFunctor.Build [the homType of (C * C)%type] C fst
+     (fun (a b : C * C) (f : a ~> b) => f.1).
+HB.instance Definition _ (C : Hom.type) :=
+  IsPreFunctor.Build [the homType of (C * C)%type] C snd
+     (fun (a b : C * C) (f : a ~> b) => f.2).
+
+Definition prod3l {C : PreMonoidal.type} (x : C * C * C) : C :=
+  (x.1.1 * x.1.2) * x.2.
+HB.instance Definition _ {C : PreMonoidal.type} :=
+  IsPreFunctor.Build _ C prod3l
+   (fun a b (f : a ~> b) => (f.1.1 ** f.1.2) ** f.2).
+
+Definition prod3r {C : PreMonoidal.type} (x : C * C * C) : C :=
+  x.1.1 * (x.1.2 * x.2).
+HB.instance Definition _ {C : PreMonoidal.type} :=
+  IsPreFunctor.Build _ C prod3r
+   (fun a b (f : a ~> b) => f.1.1 ** (f.1.2 ** f.2)).
+
+Definition prod1r {C : PreMonoidal.type} (x : C) : C := 1 * x.
+HB.instance Definition _ {C : PreMonoidal.type} :=
+  IsPreFunctor.Build [the homType of C : Type] C prod1r
+   (fun (a b : C) (f : a ~> b) => \idmap_1 ** f).
+
+Definition prod1l {C : PreMonoidal.type} (x : C) : C := x * 1.
+HB.instance Definition _ {C : PreMonoidal.type} :=
+  IsPreFunctor.Build [the homType of C : Type] C prod1l
+   (fun (a b : C) (f : a ~> b) => f ** \idmap_1).
+
+HB.mixin Record PreMonoidal_IsMonoidal C of PreMonoidal C := {
+  prodA  : prod3l ~~> prod3r :> _ ~> C;
+  prod1c : prod1r ~~> idfun :> C ~> C;
+  prodc1 : prod1l ~~> idfun :> C ~> C;
+  prodc1c : forall (x y : C),
+      prodA (x, 1, y) \; \idmap_x ** prod1c y = prodc1 x ** \idmap_y;
+  prodA4 : forall (w x y z : C),
+      prodA (w * x, y, z) \; prodA (w, x, y * z) =
+        prodA (w, x, y) ** \idmap_z \; prodA (w, x * y, z) \; \idmap_w ** prodA (x, y, z);
+}.
+
+Un
+
+HB.structure Definition Monoidal : Set :=
+  { C of PreMonoidal_IsMonoidal C & PreMonoidal C }.
+
+
+
+
diff --git a/structures.v b/structures.v
index 8dcb68a88..136afe5f7 100644
--- a/structures.v
+++ b/structures.v
@@ -442,7 +442,7 @@ Elpi Accumulate File "HB/factory.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate lp:{{
 
-main [A] :- A = indt-decl _, !,
+main [A] :- (A = indt-decl _; A = upoly-indt-decl _ _), !,
   with-attributes (with-logging (factory.declare-mixin A)).
 
 main _ :-
@@ -610,12 +610,15 @@ Elpi Accumulate File "HB/structure.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate lp:{{
 
-main [const-decl N (some B) Arity] :- !, std.do! [
+main [A] :- with-upoly-argument A main.aux.
+
+main.aux (const-decl N (some B) Arity) :- std.do! [
   prod-last {coq.arity->term Arity} Ty,
   if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort,
   with-attributes (with-logging (structure.declare N B Univ))
 ].
-main _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
+
+main.aux _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
 
 }}.
 Elpi Typecheck.