diff --git a/Changelog.md b/Changelog.md
index 362635347..bd2b83fb4 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -4,12 +4,78 @@
 
 Requires Elpi 1.15.0 and Coq 8.16.
 
+The main changes are:
+- experimental support for universe polymorphism
+- command arguments are elaborated by Coq (unless told otherwise)
+
 ### HOAS
-- Change arguments are passed after elaboration
-- New attribute `#[arguments(raw)]` to get arguments in raw format
+- Change arguments to commands are elaborated by Coq
+- New attribute `#[arguments(raw)]` to get arguments in raw format (as in
+  version 1.14 or below)
 - Change raw inductive declaration using `|` to mark non-uniform
   parameters is expected to not pass uniform parameters to the inductive
-  type (the same behavior applies to elaborated arguments)
+  type (the same behavior applies to elaborated arguments, making the two
+  consistent)
+- New `pglobal` term constructor carrying a `gref` and a `univ-instance` for
+  universe polymorphic terms
+- New `upoly-indt-decl` argument type for polymorphic inductive types
+  declarations
+- New `upoly-const-decl` argument type for polymorphic definitions
+- New `upoly-decl` data type for universe parameters declarations, i.e.
+  the `@{u1 u2 | u1 < u2}` Coq syntax one can use for inductives or definitions
+- New `upoly-decl-cumul` data type for universe parameters declarations, i.e.
+  the `@{u1 u2 | u1 < u2}` Coq syntax one can use for cumulative inductives
+- Rename `univ` -> `sort` i.e. `(sort S)` is a `term` and `S` can be `prop` or
+  `(type U)` where `U` is a `univ`
+- New `univ-instance` opaque type to represent how a polymorphic constant is
+  instantiated, i.e. `(pglobal GR I)` where `GR` is a `gref` and `I` a
+  `univ-instance`
+- New `univ-variable` opaque type for `univ` which are not algebraic. This data
+  type is used in `upoly-decl` and `upoly-decl-cumul`
+
+### API
+- New `@uinstance!` attribute supported by many `coq.env.*` APIs that can be
+  used to read/write the universe instance of polymorphic constants. E.g.
+  `@uinstance! UI => coq.env.typeof GR Ty` can instantiate `Ty` to `UI` if
+  provided or set `UI` to a fresh instance if not
+- New `@udecl!` attribute to declare polymorphic constants or inductives,
+  like the `@{u1 u2 | u1 < u2}` Coq syntax
+- New `@udecl-cumul!` attribute to declare polymorphic inductives,
+  like the `@{+u1 u2 | u1 < u2}` Coq syntax
+- New `@univpoly!` shorter version of `@udecl!`,
+  like the `#[universes(polymorphic)]` Coq syntax (without giving any other
+  `@{u1 u2 | u1 < u2}` directive)
+- New `@univpoly-cumul!` shorter version of `@udecl-cumul!`, like
+  the `#[universes(polymorphic,cumulative)]` Coq syntax
+- New `coq.env.global` API to craft a `term` from a `gref`. When used with
+  spilling `{coq.env.global GR}` gives either `(global GR)` or `(pglobal GR I)`
+  depending on `GR` being universe polymorphic or not. It understands the
+  `@unistance!` attribute for both reading or setting `I`
+- New `coq.env.univpoly?` to tell if a `gref` is universe polymorphic and how
+  many parameters it has
+- Change `coq.univ.leq` -> `coq.sort.leq`
+- Change `coq.univ.eq` -> `coq.sort.eq`
+- Change `coq.univ.sup` -> `coq.sort.sup`
+- New `coq.sort.pts-triple` computes the resulting `sort` of a product
+- New `coq.univ.constraints` gives all the universe constraints in a first class
+  form
+- Change `coq.univ.new` does not take a list anymore
+- New `coq.univ` to find a global universe
+- New `coq.univ.global?` tests if a universe is global
+- New `coq.univ.variable` links a `univ` to a `univ-variable` (imposing an
+  equality constraint if needed)
+- New `coq.univ.variable.constraints` finds all constraints talking about a
+  variable
+- New `coq.univ-instance` links a `univ-instance` to a list of of
+  `univ-variable`
+- New `coq.univ-instance.unify-eq` unifies two `univ-instance`
+  (for the same `gref`)
+- New `coq.univ-instance.unify-leq` unifies two `univ-instance`
+  (for the same `gref`)
+- New `coq.univ.set` OCaml's set for `univ`
+- New `coq.univ.map` OCaml's map for `univ`
+- New `coq.univ-variable.set` OCaml's set for `univ-variable`
+- New `coq.univ-variable.map` OCaml's map for `univ-variable`
 
 ### Vernacular
 - New `Accumulate File <ident>` to be used in tandem with Coq 8.16
diff --git a/apps/derive/elpi/cast.elpi b/apps/derive/elpi/cast.elpi
index 24b5686a1..b3703c590 100644
--- a/apps/derive/elpi/cast.elpi
+++ b/apps/derive/elpi/cast.elpi
@@ -8,7 +8,7 @@ namespace derive.cast {
 
 namespace aux {
 
-arity [] _ (sort (typ U)) :- coq.univ.new [] U.
+arity [] _ (sort (typ U)) :- coq.univ.new U.
 arity [V|VS] Acc (prod `x` T R) :-
   coq.mk-app V {rev Acc} T,
   pi x\ arity VS [x|Acc] (R x).
diff --git a/apps/derive/elpi/induction.elpi b/apps/derive/elpi/induction.elpi
index 2c77b7ac0..c5b02b9a2 100644
--- a/apps/derive/elpi/induction.elpi
+++ b/apps/derive/elpi/induction.elpi
@@ -78,7 +78,7 @@ hyps [] [] Ity Arity (fix `IH` Recno Fty Bo) :-
 
 pred truncated-predicate-ty i:term, o:term.
 truncated-predicate-ty (sort _) T :- informative, !,
-  T = sort (typ U), coq.univ.new [] U.
+  T = sort (typ U), coq.univ.new U.
 truncated-predicate-ty (sort _) (sort prop).
 
 truncated-predicate-ty (prod N S T) (prod N S R) :-
diff --git a/apps/derive/elpi/param1.elpi b/apps/derive/elpi/param1.elpi
index 4a250b7de..601442042 100644
--- a/apps/derive/elpi/param1.elpi
+++ b/apps/derive/elpi/param1.elpi
@@ -12,7 +12,7 @@ coq.subst-fun XS T TXS :- !, coq.mk-app T XS TXS.
 % this is outside the namespace since the predicate is also the db-one
 reali (sort prop as P) (fun `s` P x\ prod `s1` x _\ P) :- !.
 reali (sort _) (fun `s` (sort (typ U)) x\ prod `s1` x _\ (sort (typ V))) :- !,
-  coq.univ.new [] U, coq.univ.new [] V.
+  coq.univ.new U, coq.univ.new V.
 
 reali (fun N T B) (fun N T x\ fun N1 (TRsubst x) xR\ BR x xR) :- !, do! [
   coq.name-suffix `P` N N1,
diff --git a/apps/derive/elpi/param2.elpi b/apps/derive/elpi/param2.elpi
index 6648ed238..17fef0719 100644
--- a/apps/derive/elpi/param2.elpi
+++ b/apps/derive/elpi/param2.elpi
@@ -13,7 +13,7 @@ coq.subst-fun XS T TXS :- !, coq.mk-app T XS TXS.
 param (sort prop as P) P (fun `s` P x\ fun `s` P y\ prod `s1` x _\ prod `s2` y _\ P) :- !.
 param (sort _ as P) P
   (fun `u` (sort (typ U)) x\ fun `v` (sort (typ V)) y\ prod `s1` x _\ prod `s2` y _\ P) :- !,
-  coq.univ.new [] U, coq.univ.new [] V.
+  coq.univ.new U, coq.univ.new V.
 
 param (fun N T B) (fun N T1 B1)
       (fun N T x\ fun N T1 x1\ fun N (TRsubst x x1) xR\ BR x x1 xR) :- !, do! [
diff --git a/apps/locker/elpi/locker.elpi b/apps/locker/elpi/locker.elpi
index dc44d0bf8..f105397f7 100644
--- a/apps/locker/elpi/locker.elpi
+++ b/apps/locker/elpi/locker.elpi
@@ -4,23 +4,25 @@
 
 namespace locker {
 
-pred key-lock i:id, i:term, i:arity.
-key-lock ID BoSkel AritySkel :- std.do! [
+pred key-lock i:id, i:term, i:arity, i:option upoly-decl.
+key-lock ID Bo Arity UnivDecl :- std.spy-do! [
   make-key ID Key,
 
-  coq.arity->term AritySkel TySkel,
+  coq.arity->term Arity Ty,
+  Def = {{ @locked_with lp:Key lp:Ty lp:Bo }},
   std.assert-ok!
-    (coq.elaborate-skeleton
-      {{ @locked_with lp:Key lp:TySkel lp:BoSkel }} DefTy Def)
+    (coq.typecheck Def _)
     "locker: illtyped definition",
-  coq.env.add-const ID Def DefTy @transparent! C,
 
-  coq.arity->implicits AritySkel CImpls,
+  if (UnivDecl = some UD) (coq.upoly-decl->attribute UD Poly!) (Poly! = true),
+  Poly! => coq.env.add-const ID Def Ty @transparent! C,
+
+  coq.arity->implicits Arity CImpls,
   if (coq.any-implicit? CImpls)
      (coq.arguments.set-implicit (const C) [CImpls])
      true,
 
-  make-key-unlockable ID Def DefTy (global (const C)) Key,
+  make-key-unlockable ID Def Ty {coq.env.global (const C)} Key,
 ].
 
 pred make-key i:id, o:term.
@@ -31,16 +33,26 @@ make-key ID (global (const C)) :- std.do! [
 
 % -------------------------------------------------------------------------
 
-pred module-lock i:id, i:term, i:arity.
-module-lock ID BoSkel AritySkel :- std.do! [
-  std.assert-ok! (coq.elaborate-arity-skeleton AritySkel _ Arity)
-    "locker: definition type illtyped",
+pred module-lock i:id, i:term, i:arity, i:option upoly-decl.
+module-lock ID Bo Arity UnivDecl :- std.do! [
   coq.arity->term Arity Ty,
-  std.assert-ok! (coq.elaborate-skeleton BoSkel Ty Bo)
-    "locker: definition body illtyped",
-
-  lock-module-type ID Ty Bo Signature,
-  lock-module-body Signature ID Ty Bo Symbol Module,
+  std.assert-ok! (coq.typecheck-ty Ty _) "locker: definition type illtyped",
+  std.assert-ok! (coq.typecheck Bo Ty) "locker: definition body illtyped",
+
+  % we craft all constants now since we need to put *in the interface* the
+  % extra universe constraints (if upoly) which are necessary for the body!
+  if (UnivDecl = some UD)
+    (std.do![
+      PTY = {{ lp:Bo = lp:Bo }},
+      std.assert-ok! (coq.typecheck-ty PTY _) "lock: unlock statement illtyped",
+      P = {{ @refl_equal lp:Ty lp:Bo }},
+      std.assert-ok! (coq.typecheck P PTY) "locker: unlock proof illtyped",
+      coq.upoly-decl.complete-constraints UD UD1,
+      UnivDecl1 = some UD1])
+    (UnivDecl1 = none),
+
+  lock-module-type ID Ty Bo UnivDecl1 Signature,
+  lock-module-body Signature ID Ty Bo UnivDecl1 Symbol Module,
 
   @global! => coq.notation.add-abbreviation ID 0 Symbol ff _,
 
@@ -52,27 +64,31 @@ module-lock ID BoSkel AritySkel :- std.do! [
   make-module-unlockable ID Module,
 ].
 
-pred lock-module-type i:id, i:term, i:term, o:modtypath.
-lock-module-type ID Ty Bo M :- std.do! [
+pred lock-module-type i:id, i:term, i:term, i:option upoly-decl, o:modtypath.
+lock-module-type ID Ty Bo UnivDecl M :- std.do! [
   Module is ID ^ "_Locked",
   coq.env.begin-module-type Module,
-  coq.env.add-axiom "body" Ty C, B = global (const C),
+  if (UnivDecl = some UD) (coq.upoly-decl->attribute UD Poly!) (Poly! = true),
+  Poly! => coq.env.add-axiom "body" Ty C, coq.env.global (const C) B,
   PTY = {{ lp:B = lp:Bo }},
   std.assert-ok! (coq.typecheck-ty PTY _) "lock: unlock statement illtyped",
-  coq.env.add-axiom "unlock" PTY _,
+  if (UnivDecl = some UD) (coq.upoly-decl.complete-constraints UD UD1, coq.upoly-decl->attribute UD1 Poly1!) (Poly1! = true),
+  Poly1! => coq.env.add-axiom "unlock" PTY _,
   coq.env.end-module-type M,
 ].
 
-pred lock-module-body o:modtypath, i:id, i:term, i:term, o:term, o:modpath.
-lock-module-body Signature ID Ty Bo B M :- std.do! [
+pred lock-module-body o:modtypath, i:id, i:term, i:term, i:option upoly-decl, o:term, o:modpath.
+lock-module-body Signature ID Ty Bo UnivDecl B M :- std.do! [
   coq.env.begin-module ID (some Signature),
-  coq.env.add-const "body" Bo Ty @transparent! C,
-  B = global (const C),
+  if (UnivDecl = some UD) (coq.upoly-decl->attribute UD Poly!) (Poly! = true),
+  Poly! => coq.env.add-const "body" Bo Ty @transparent! C,
+  coq.env.global (const C) B,
   P = {{ @refl_equal lp:Ty lp:B }},
   std.assert-ok! (coq.typecheck P _) "locker: unlock proof illtyped",
   PTY = {{ lp:B = lp:Bo }},
   std.assert-ok! (coq.typecheck-ty PTY _) "locker: unlock statement illtyped",
-  coq.env.add-const "unlock" P PTY @opaque! _,
+  if (UnivDecl = some UD) (coq.upoly-decl.complete-constraints UD UD1, coq.upoly-decl->attribute UD1 Poly1!) (Poly1! = true),
+  Poly1! => coq.env.add-const "unlock" P PTY @opaque! _,
   coq.env.end-module M,
 ].
 
@@ -80,10 +96,10 @@ lock-module-body Signature ID Ty Bo B M :- std.do! [
 % Unlocking via the ssreflect Unlockable interface (CS instance)
 
 pred make-key-unlockable i:string, i:term, i:term, i:term, i:term.
-make-key-unlockable ID DefBo DefTy LockedDef Key :- std.do! [
+make-key-unlockable ID DefBo Ty LockedDef Key :- std.do! [
   % we extract the real body in order to be precise in the unlocking equation
   DefBo = {{ @locked_with _ _ lp:Bo }},
-  UnlockEQ = {{ @locked_withE lp:DefTy lp:Key lp:Bo }},
+  UnlockEQ = {{ @locked_withE lp:Ty lp:Key lp:Bo }},
   Unlock = {{ @Unlockable _ _ lp:LockedDef lp:UnlockEQ }},
   make-unlockable ID Unlock,
 ].
@@ -91,7 +107,8 @@ make-key-unlockable ID DefBo DefTy LockedDef Key :- std.do! [
 pred make-module-unlockable i:id, i:modpath.
 make-module-unlockable ID Module :- std.do! [
   coq.env.module Module [_,UnlockEQ],
-  Unlock = {{ Unlockable lp:{{ global UnlockEQ }} }},
+  coq.env.global UnlockEQ UnlockEQT,
+  Unlock = {{ Unlockable lp:UnlockEQT }},
   make-unlockable ID Unlock,
 ].
 
diff --git a/apps/locker/tests/test_locker.v b/apps/locker/tests/test_locker.v
index 340d8786e..4d6dad809 100644
--- a/apps/locker/tests/test_locker.v
+++ b/apps/locker/tests/test_locker.v
@@ -62,3 +62,17 @@ Module elab.
 mlock Definition y (z : nat) := ltac:(exact z).
 mlock Definition q (b : bool) := if b then 1 else 0.
 End elab.
+
+(* ----------------------- *)
+
+Set Printing Universes.
+
+lock #[universes(polymorphic)] Definition id1@{u} (T : Type@{u}) (x : T) := x.
+About id1.
+
+mlock #[universes(polymorphic)] Definition id2@{u} (T : Type@{u}) (x : T) := x.
+About id2.
+About id2.body.
+(* id2.body@{u} : forall T : Type@{u}, T -> T
+    (* u |= u < eq.u0 *)
+*)
\ No newline at end of file
diff --git a/apps/locker/theories/locker.v b/apps/locker/theories/locker.v
index 6987e53ff..0e433d1b7 100644
--- a/apps/locker/theories/locker.v
+++ b/apps/locker/theories/locker.v
@@ -37,7 +37,13 @@ Elpi Accumulate lp:{{
     coq.parse-attributes A [
       att "key" string,
     ] Opts, !,
-    Opts => locker.key-lock ID Bo Ty.
+    Opts => locker.key-lock ID Bo Ty none.
+  main [upoly-const-decl ID (some Bo) Ty UnivDecl] :- !,
+    attributes A,
+    coq.parse-attributes A [
+      att "key" string,
+    ] Opts, !,
+    Opts => locker.key-lock ID Bo Ty (some UnivDecl).
   main _ :- coq.error "Usage: lock Definition ...".
 }}.
 Elpi Typecheck.
@@ -67,7 +73,8 @@ mlock Definition foo : T := bo.
 Elpi Command mlock.
 Elpi Accumulate File locker.
 Elpi Accumulate lp:{{
-  main [const-decl ID (some Bo) Ty] :- !, locker.module-lock ID Bo Ty.
+  main [const-decl ID (some Bo) Ty] :- !, locker.module-lock ID Bo Ty none.
+  main [upoly-const-decl ID (some Bo) Ty UD] :- !, locker.module-lock ID Bo Ty (some UD).
   main _ :- coq.error "Usage: mlock Definition ...".
 }}.
 Elpi Typecheck.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index 7f396a049..fc3ea117e 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -57,8 +57,11 @@ type trm       term   -> argument. % Eg. (t).
 %
 % Eg. Record m A : T := K { f : t; .. }.
 type indt-decl indt-decl -> argument.
+type upoly-indt-decl indt-decl -> upoly-decl -> argument.
+type upoly-indt-decl indt-decl -> upoly-decl-cumul -> argument.
 % Eg. Definition m A : T := B. (or Axiom when the body is none)
 type const-decl id -> option term -> arity -> argument.
+type upoly-const-decl id -> option term -> arity -> upoly-decl -> argument.
 % Eg. Context A (b : A).
 type ctx-decl context-decl -> argument.
 
@@ -71,10 +74,11 @@ type ctx-decl context-decl -> argument.
 % -- terms --------------------------------------------------------------------
 kind term type.
 
-type sort  universe -> term. % Prop, Type@{i}
+type sort  sort -> term. % Prop, Type@{i}
 
 % constants: inductive types, inductive constructors, definitions
 type global gref -> term.
+type pglobal gref -> univ-instance -> term.
 
 % binders: to form functions, arities and local definitions
 type fun  name -> term -> (term -> term) -> term.         % fun x : t =>
@@ -352,6 +356,13 @@ macro @local!    :- get-option "coq:locality" "local".
 
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 
+macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance
+
+macro @udecl! Vs LV Cs LC       :- get-option "coq:udecl" (upoly-decl Vs LV Cs LC).
+macro @udecl-cumul! Vs LV Cs LC :- get-option "coq:udecl-cumul" (upoly-decl-cumul Vs LV Cs LC).
+macro @univpoly!       :- @udecl! [] tt [] tt.
+macro @univpoly-cumul! :- @udecl-cumul! [] tt [] tt.
+
 macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width
 macro @ppall! :- get-option "coq:pp" "all". % printing all
 macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents
@@ -561,9 +572,20 @@ external pred coq.locate-all i:id, o:list located.
 external pred coq.locate i:id, o:gref.
 
 % [coq.env.typeof GR Ty] reads the type Ty of a global reference.
+% Supported attributes:
+% - @uinstance! I (default: fresh instance I)
 external pred coq.env.typeof i:gref, o:term.
 
-external pred coq.env.indt % reads the inductive type declaration for the environment
+% [coq.env.global GR T] turns a global reference GR into a term.
+% T = (global GR) or, if GR points to a universe polymorphic term,
+% T = (pglobal GR I).
+% Supported attributes:
+% - @uinstance! I (default: fresh instance I)
+external pred coq.env.global i:gref, o:term.
+
+external pred coq.env.indt % reads the inductive type declaration for the environment.
+% Supported attributes:
+% - @uinstance! I (default: fresh instance I)
   i:inductive,        % reference to the inductive type
   o:bool,             % tt if the type is inductive (ff for co-inductive)
   o:int,              % number of parameters
@@ -572,14 +594,18 @@ external pred coq.env.indt % reads the inductive type declaration for the enviro
   o:list constructor, % list of constructor names
   o:list term.        % list of the types of the constructors (type of KNames) including parameters
   
-external pred coq.env.indt-decl % reads the inductive type declaration for the environment
+external pred coq.env.indt-decl % reads the inductive type declaration for the environment.
+% Supported attributes:
+% - @uinstance! I (default: fresh instance I)
   i:inductive, % reference to the inductive type
   o:indt-decl. % HOAS description of the inductive type
   
 % [coq.env.indc GR ParamNo UnifParamNo Kno Ty] reads the type Ty of an
-% inductive constructor GR, as well as the number of parameters ParamNo and
-% uniform parameters UnifParamNo and the number of the constructor Kno (0
-% based)
+% inductive constructor GR, as well as
+% the number of parameters ParamNo and uniform parameters
+% UnifParamNo and the number of the constructor Kno (0 based).
+% Supported attributes:
+% - @uinstance! I (default: fresh instance I)
 external pred coq.env.indc i:constructor, o:int, o:int, o:int, o:term.
 
 % [coq.env.informative? Ind] Checks if Ind is informative, that is, if
@@ -599,12 +625,22 @@ external pred coq.env.recursive? i:inductive.
 % [coq.env.opaque? GR] checks if GR is an opaque constant
 external pred coq.env.opaque? i:constant.
 
-% [coq.env.const GR Bo Ty] reads the type Ty and the body Bo of constant GR.
+% [coq.env.univpoly? GR PolyArity] checks if GR is universe polymorphic and
+% if so returns the number of universe variables
+external pred coq.env.univpoly? i:gref, o:int.
+
+% [coq.env.const GR Bo Ty] reads the type Ty and the body Bo of constant
+% GR.
 % Opaque constants have Bo = none.
+% Supported attributes:
+% - @uinstance! I (default: fresh instance I)
 external pred coq.env.const i:constant, o:option term, o:term.
 
 % [coq.env.const-body GR Bo] reads the body of a constant, even if it is
-% opaque. If such body is none, then the constant is a true axiom
+% opaque.
+% If such body is none, then the constant is a true axiom.
+% Supported attributes:
+% - @uinstance! I (default: fresh instance I)
 external pred coq.env.const-body i:constant, o:option term.
 
 % [coq.env.primitive? GR] tests if GR is a primitive constant (like uin63
@@ -650,9 +686,11 @@ external pred coq.env.current-path o:list string.
 
 % -- Environment: write -----------------------------------------------
 
-% Note: universe constraints are taken from ELPI's constraints store. Use
-% coq.univ-* in order to add constraints (or any higher level facility as
-% coq.typecheck)
+% Note: (monomorphic) universe constraints are taken from ELPI's
+% constraints store. Use coq.univ-* in order to add constraints (or any
+% higher level facility as coq.typecheck). Load in the context attributes
+% such as @univpoly!, @univpoly-cumul!, @udecl! or @udecl-cumul! in order to
+% declare universe polymorphic constants or inductives.
 
 % [coq.env.add-const Name Bo Ty Opaque C] Declare a new constant: C gets a
 % constant derived from Name
@@ -670,6 +708,9 @@ external pred coq.env.current-path o:list string.
 % Supported attributes:
 % - @local! (default: false)
 % - @using! (default: section variables actually used)
+% - @univpoly! (default unset)
+% - @udecl! (default unset)
+% 
 external pred coq.env.add-const i:id, i:term, i:term, i:opaque?, 
                                 o:constant.
 
@@ -678,10 +719,10 @@ external pred coq.env.add-const i:id, i:term, i:term, i:opaque?,
 % and the current module.
 % Supported attributes:
 % - @local! (default: false)
+% - @univpoly! (default unset)
 % - @using! (default: section variables actually used)
 % - @inline! (default: no inlining)
 % - @inline-at! N (default: no inlining)
-% 
 external pred coq.env.add-axiom i:id, i:term, o:constant.
 
 % [coq.env.add-section-variable Name Ty C] Declare a new section variable: C
@@ -790,36 +831,158 @@ external pred coq.env.projections i:inductive, o:list (option constant).
 external pred coq.env.primitive-projections i:inductive, 
                                             o:list (option (pair projection int)).
 
-% -- Universes --------------------------------------------------------
+% -- Sorts (and their universe level, if applicable) ----------------
 
-% universe level
+% Warning: universe polymorphism has to be considered experimental *E* as
+% a feature, not just as a set of APIs. Unfortunately some of the
+% current complexity is exposed to the programmer, bare with us.
+% 
+% The big bang is that in Coq one has terms, types and sorts (which are
+% the types of types). Some sorts (as of today only Type) some with
+% a universe level, on paper Type_i for some i. At the sort level
+% Coq features some form of subtyping: a function expecting a function
+% to Type, e.g. nat -> Type, can receive a function to Prop, since
+% Prop <= Type. So far, so good. But what are these levels i
+% exactly?
+% 
+% Universe levels are said to be "algebraic", they are made of
+% variables (see the next section) and the two operators +1 and max.
+% This is a sort of internal optimization that leaks to the
+% user/programmer. Indeed these universe levels cannot be (directly) used
+% in all APIs morally expecting a universe level "i", in particular
+% the current constraint engine cannot handle constraint with an
+% algebraic level on the right, e.g. i <= j+1. Since some APIs only
+% accept universe variables, we provide the coq.univ.variable API
+% which is able to craft a universe variable which is roughly
+% equivalent to an algebraic universe, e.g. k such that j+1 = k.
+% 
+% Coq-Elpi systematically purges algebraic universes from terms (and
+% types and sorts) when one reads them from the environment. This
+% makes the embedding of terms less precise than what it could be.
+% The different data types stay, since Coq will eventually become
+% able to handle algebraic universes consistently, making this purging
+% phase unnecessary.
+
+% universe level (algebraic: max, +1, univ-variable)
 typeabbrev univ (ctype "univ").
 
 
-% Universes (for the sort term former)
-kind universe type.
-type prop universe. % impredicative sort of propositions
-type sprop universe. % impredicative sort of propositions with definitional proof irrelevance
-type typ univ -> universe. % predicative sort of data (carries a level)
+% Sorts (kinds of types)
+kind sort type.
+type prop sort. % impredicative sort of propositions
+type sprop sort. % impredicative sort of propositions with definitional proof irrelevance
+type typ univ ->
+         sort. % predicative sort of data (carries a universe level)
+
+% [coq.sort.leq S1 S2] constrains S1 <= S2
+external pred coq.sort.leq o:sort, o:sort.
+
+% [coq.sort.eq S1 S2] constrains S1 = S2
+external pred coq.sort.eq o:sort, o:sort.
+
+% [coq.sort.sup S1 S2] constrains S2 = S1 + 1
+external pred coq.sort.sup o:sort, o:sort.
+
+% [coq.sort.pts-triple S1 S2 S3] constrains S3 = sort of product with domain
+% in S1 and codomain in S2
+external pred coq.sort.pts-triple o:sort, o:sort, o:sort.
 
 % [coq.univ.print] prints the set of universe constraints
 external pred coq.univ.print .
 
-% [coq.univ.leq U1 U2] constrains U1 <= U2
-external pred coq.univ.leq i:univ, i:univ.
+% [coq.univ.new U] A fresh universe.
+external pred coq.univ.new o:univ.
+
+% [coq.univ Name U] Finds a named unvierse. Can fail.
+external pred coq.univ o:id, o:univ.
+
+% [coq.univ.global? U] succeeds if U is a global universe
+external pred coq.univ.global? i:univ.
+
+% [coq.univ.constraints CL] gives the list of constraints, see also
+% coq.univ.variable.constraints
+external pred coq.univ.constraints o:list univ-constraint.
+
+% -- Universe variables ------
 
-% [coq.univ.eq U1 U2] constrains U1 = U2
-external pred coq.univ.eq i:univ, i:univ.
+% universe level variable
+typeabbrev univ-variable (ctype "univ-variable").
 
-% [coq.univ.new Names U] fresh universe *E*
-external pred coq.univ.new i:list id, o:univ.
 
-% [coq.univ.sup U1 U2] constrains U2 = U1 + 1
-external pred coq.univ.sup i:univ, i:univ.
+% [coq.univ.variable U L] relates a univ-variable L to a univ U
+external pred coq.univ.variable o:univ, o:univ-variable.
+
+% [coq.univ.variable.constraints L CL] gives the list of constraints on L.
+% Can be used to craft a strict upoly-decl
+external pred coq.univ.variable.constraints i:univ-variable, 
+                                            o:list univ-constraint.
+
+% -- Universe instance (for universe polymorphic global terms) ------
+
+% As of today a universe polymorphic constant can only be instantiated
+% with universe level variables. That is f@{Prop} is not valid, nor
+% is f@{u+1}. One can only write f@{u} for any u.
+% 
+% A univ-instance is morally a list of universe level variables,
+% but its list syntax is hidden in the terms. If you really need to
+% craft or inspect one of these, the following APIs can help you.
+% 
+% Most of the time the user is expected to use coq.env.global which
+% crafts a fresh, appropriate, universe instance and possibly unify that
+% term (of the instance it contains) with another one.
 
-% [coq.univ.pts-triple U1 U2 U3] constrains U3 = universe of product with
-% domain in U1 and codomain in U2)
-external pred coq.univ.pts-triple i:univ, i:univ, o:univ.
+% Universes level instance for a universe-polymoprhic constant
+typeabbrev univ-instance (ctype "univ-instance").
+
+
+% [coq.univ-instance UI UL] relates a univ-instance UI and a list of
+% universe level variables UL
+external pred coq.univ-instance o:univ-instance, o:list univ-variable.
+
+% [coq.univ-instance.unify-eq GR UI1 UI2 Diagnostic] unifies the two
+% universe instances for the same gref
+external pred coq.univ-instance.unify-eq i:gref, i:univ-instance, 
+                                         i:univ-instance, o:diagnostic.
+
+% [coq.univ-instance.unify-leq GR UI1 UI2 Diagnostic] unifies the two
+% universe instances for the same gref. Note: if the GR is not *cumulative*
+% (see Cumulative or #[universes(cumulative)]) then this API imposes an
+% equality constraint.
+external pred coq.univ-instance.unify-leq i:gref, i:univ-instance, 
+                                          i:univ-instance, o:diagnostic.
+
+% -- Declaration of universe polymorphic global terms -----------
+
+% These are the data types used to declare how constants
+% and inductive types should be declared (see also the @udecl!
+% and
+% @udecl-cumul! macros). Note that only inductive types can be
+% declared as cumulative.
+
+% Constraint between two universes level variables
+kind univ-constraint type.
+type lt univ-variable -> univ-variable -> univ-constraint.
+type le univ-variable -> univ-variable -> univ-constraint.
+type eq univ-variable -> univ-variable -> univ-constraint.
+
+% Variance of a universe level variable
+kind univ-variance type.
+type auto univ-variable -> univ-variance.
+type covariant univ-variable -> univ-variance.
+type invariant univ-variable -> univ-variance.
+type irrelevant univ-variable -> univ-variance.
+
+% Constraints for a non-cumulative declaration. Boolean tt means loose
+% (e.g. the '+' in f@{u v + | u < v +})
+kind upoly-decl type.
+type upoly-decl list univ-variable -> bool -> list univ-constraint ->
+                bool -> upoly-decl.
+
+% Constraints for a cumulative declaration. Boolean tt means loose (e.g.
+% the '+' in f@{u v + | u < v +})
+kind upoly-decl-cumul type.
+type upoly-decl-cumul list univ-variance -> bool ->
+                      list univ-constraint -> bool -> upoly-decl-cumul.
 
 % -- Primitive --------------------------------------------------------
 
@@ -859,7 +1022,7 @@ kind cs-pattern type.
 type cs-gref gref -> cs-pattern.
 type cs-prod cs-pattern.
 type cs-default cs-pattern.
-type cs-sort universe -> cs-pattern.
+type cs-sort sort -> cs-pattern.
 
 % Canonical Structure instances: (cs-instance Proj ValPat Inst)
 kind cs-instance type.
@@ -1127,7 +1290,7 @@ external pred coq.typecheck i:term, o:term, o:diagnostic.
 % universe U. If U is provided, then
 % the inferred universe is unified (see unify-leq) with it.
 % Universe constraints are put in the constraint store.
-external pred coq.typecheck-ty i:term, o:universe, o:diagnostic.
+external pred coq.typecheck-ty i:term, o:sort, o:diagnostic.
 
 % [coq.unify-eq A B Diagnostic] unifies the two terms
 external pred coq.unify-eq i:term, i:term, o:diagnostic.
@@ -1148,7 +1311,7 @@ external pred coq.elaborate-skeleton i:term, o:term, o:term, o:diagnostic.
 % T is allowed to contain holes (unification variables) but these are
 % not assigned even if the elaborated term has a term in place of the
 % hole. Similarly universe levels present in T are disregarded.
-external pred coq.elaborate-ty-skeleton i:term, o:universe, o:term, 
+external pred coq.elaborate-ty-skeleton i:term, o:sort, o:term, 
                                         o:diagnostic.
 
 % -- Coq's reduction machines ------------------------------------
@@ -1441,6 +1604,150 @@ external pred coq.gref.map.find i:gref, i:coq.gref.map A, o:A.
 external pred coq.gref.map.bindings i:coq.gref.map A, 
                                     o:list (pair gref A).
 
+kind coq.univ.set type.
+
+% [coq.univ.set.empty A] The empty set
+external pred coq.univ.set.empty o:coq.univ.set.
+
+% [coq.univ.set.mem Elem A] Checks if Elem is in a
+external pred coq.univ.set.mem i:univ, i:coq.univ.set.
+
+% [coq.univ.set.add Elem A B] B is A union {Elem}
+external pred coq.univ.set.add i:univ, i:coq.univ.set, o:coq.univ.set.
+
+% [coq.univ.set.remove Elem A B] B is A \ {Elem}
+external pred coq.univ.set.remove i:univ, i:coq.univ.set, o:coq.univ.set.
+
+% [coq.univ.set.union A B X] X is A union B
+external pred coq.univ.set.union i:coq.univ.set, i:coq.univ.set, 
+                                 o:coq.univ.set.
+
+% [coq.univ.set.inter A B X] X is A intersection B
+external pred coq.univ.set.inter i:coq.univ.set, i:coq.univ.set, 
+                                 o:coq.univ.set.
+
+% [coq.univ.set.diff A B X] X is A \ B
+external pred coq.univ.set.diff i:coq.univ.set, i:coq.univ.set, 
+                                o:coq.univ.set.
+
+% [coq.univ.set.equal A B] tests A and B for equality
+external pred coq.univ.set.equal i:coq.univ.set, i:coq.univ.set.
+
+% [coq.univ.set.subset A B] tests if A is a subset of B
+external pred coq.univ.set.subset i:coq.univ.set, i:coq.univ.set.
+
+% [coq.univ.set.elements M L] L is M transformed into list
+external pred coq.univ.set.elements i:coq.univ.set, o:list univ.
+
+% [coq.univ.set.cardinal M N] N is the number of elements of M
+external pred coq.univ.set.cardinal i:coq.univ.set, o:int.
+
+% CAVEAT: the type parameter of coq.univ.map must be a closed term
+
+kind coq.univ.map type -> type.
+
+% [coq.univ.map.empty M] The empty map
+external pred coq.univ.map.empty o:coq.univ.map A.
+
+% [coq.univ.map.mem S M] Checks if S is bound in M
+external pred coq.univ.map.mem i:univ, i:coq.univ.map A.
+
+% [coq.univ.map.add S V M M1] M1 is M where V is bound to S
+external pred coq.univ.map.add i:univ, i:A, i:coq.univ.map A, 
+                               o:coq.univ.map A.
+
+% [coq.univ.map.remove S M M1] M1 is M where S is unbound
+external pred coq.univ.map.remove i:univ, i:coq.univ.map A, 
+                                  o:coq.univ.map A.
+
+% [coq.univ.map.find S M V] V is the binding of S in M
+external pred coq.univ.map.find i:univ, i:coq.univ.map A, o:A.
+
+% [coq.univ.map.bindings M L] L is M transformed into an associative list
+external pred coq.univ.map.bindings i:coq.univ.map A, 
+                                    o:list (pair univ A).
+
+kind coq.univ-variable.set type.
+
+% [coq.univ-variable.set.empty A] The empty set
+external pred coq.univ-variable.set.empty o:coq.univ-variable.set.
+
+% [coq.univ-variable.set.mem Elem A] Checks if Elem is in a
+external pred coq.univ-variable.set.mem i:univ-variable, 
+                                        i:coq.univ-variable.set.
+
+% [coq.univ-variable.set.add Elem A B] B is A union {Elem}
+external pred coq.univ-variable.set.add i:univ-variable, 
+                                        i:coq.univ-variable.set, 
+                                        o:coq.univ-variable.set.
+
+% [coq.univ-variable.set.remove Elem A B] B is A \ {Elem}
+external pred coq.univ-variable.set.remove i:univ-variable, 
+                                           i:coq.univ-variable.set, 
+                                           o:coq.univ-variable.set.
+
+% [coq.univ-variable.set.union A B X] X is A union B
+external pred coq.univ-variable.set.union i:coq.univ-variable.set, 
+                                          i:coq.univ-variable.set, 
+                                          o:coq.univ-variable.set.
+
+% [coq.univ-variable.set.inter A B X] X is A intersection B
+external pred coq.univ-variable.set.inter i:coq.univ-variable.set, 
+                                          i:coq.univ-variable.set, 
+                                          o:coq.univ-variable.set.
+
+% [coq.univ-variable.set.diff A B X] X is A \ B
+external pred coq.univ-variable.set.diff i:coq.univ-variable.set, 
+                                         i:coq.univ-variable.set, 
+                                         o:coq.univ-variable.set.
+
+% [coq.univ-variable.set.equal A B] tests A and B for equality
+external pred coq.univ-variable.set.equal i:coq.univ-variable.set, 
+                                          i:coq.univ-variable.set.
+
+% [coq.univ-variable.set.subset A B] tests if A is a subset of B
+external pred coq.univ-variable.set.subset i:coq.univ-variable.set, 
+                                           i:coq.univ-variable.set.
+
+% [coq.univ-variable.set.elements M L] L is M transformed into list
+external pred coq.univ-variable.set.elements i:coq.univ-variable.set, 
+                                             o:list univ-variable.
+
+% [coq.univ-variable.set.cardinal M N] N is the number of elements of M
+external pred coq.univ-variable.set.cardinal i:coq.univ-variable.set, 
+                                             o:int.
+
+% CAVEAT: the type parameter of coq.univ-variable.map must be a closed
+% term
+
+kind coq.univ-variable.map type -> type.
+
+% [coq.univ-variable.map.empty M] The empty map
+external pred coq.univ-variable.map.empty o:coq.univ-variable.map A.
+
+% [coq.univ-variable.map.mem S M] Checks if S is bound in M
+external pred coq.univ-variable.map.mem i:univ-variable, 
+                                        i:coq.univ-variable.map A.
+
+% [coq.univ-variable.map.add S V M M1] M1 is M where V is bound to S
+external pred coq.univ-variable.map.add i:univ-variable, i:A, 
+                                        i:coq.univ-variable.map A, 
+                                        o:coq.univ-variable.map A.
+
+% [coq.univ-variable.map.remove S M M1] M1 is M where S is unbound
+external pred coq.univ-variable.map.remove i:univ-variable, 
+                                           i:coq.univ-variable.map A, 
+                                           o:coq.univ-variable.map A.
+
+% [coq.univ-variable.map.find S M V] V is the binding of S in M
+external pred coq.univ-variable.map.find i:univ-variable, 
+                                         i:coq.univ-variable.map A, o:A.
+
+% [coq.univ-variable.map.bindings M L] L is M transformed into an
+% associative list
+external pred coq.univ-variable.map.bindings i:coq.univ-variable.map A, 
+                                             o:list (pair univ-variable A).
+
 % Coq box types for pretty printing:
 % - Vertical block: each break leads to a new line
 % - Horizontal block: no line breaking
diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi
index 0d2cf87c1..cf997cc8f 100644
--- a/elpi/coq-HOAS.elpi
+++ b/elpi/coq-HOAS.elpi
@@ -42,8 +42,11 @@ type trm       term   -> argument. % Eg. (t).
 %
 % Eg. Record m A : T := K { f : t; .. }.
 type indt-decl indt-decl -> argument.
+type upoly-indt-decl indt-decl -> upoly-decl -> argument.
+type upoly-indt-decl indt-decl -> upoly-decl-cumul -> argument.
 % Eg. Definition m A : T := B. (or Axiom when the body is none)
 type const-decl id -> option term -> arity -> argument.
+type upoly-const-decl id -> option term -> arity -> upoly-decl -> argument.
 % Eg. Context A (b : A).
 type ctx-decl context-decl -> argument.
 
@@ -56,10 +59,11 @@ type ctx-decl context-decl -> argument.
 % -- terms --------------------------------------------------------------------
 kind term type.
 
-type sort  universe -> term. % Prop, Type@{i}
+type sort  sort -> term. % Prop, Type@{i}
 
 % constants: inductive types, inductive constructors, definitions
 type global gref -> term.
+type pglobal gref -> univ-instance -> term.
 
 % binders: to form functions, arities and local definitions
 type fun  name -> term -> (term -> term) -> term.         % fun x : t =>
@@ -337,6 +341,13 @@ macro @local!    :- get-option "coq:locality" "local".
 
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 
+macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance
+
+macro @udecl! Vs LV Cs LC       :- get-option "coq:udecl" (upoly-decl Vs LV Cs LC).
+macro @udecl-cumul! Vs LV Cs LC :- get-option "coq:udecl-cumul" (upoly-decl-cumul Vs LV Cs LC).
+macro @univpoly!       :- @udecl! [] tt [] tt.
+macro @univpoly-cumul! :- @udecl-cumul! [] tt [] tt.
+
 macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width
 macro @ppall! :- get-option "coq:pp" "all". % printing all
 macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents
diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi
index 8f7871f3f..74f071c5d 100644
--- a/elpi/coq-lib.elpi
+++ b/elpi/coq-lib.elpi
@@ -109,6 +109,7 @@ pred copy i:term, o:term.
 :name "copy:start"
 copy X Y :- name X, !, X = Y, !. % avoid loading "copy x x" at binders
 copy (global _ as C) C :- !.
+copy (pglobal _ _ as C) C :- !.
 copy (sort _ as C) C :- !.
 copy (fun N T F) (fun N T1 F1) :- !,
   copy T T1, pi x\ copy (F x) (F1 x).
@@ -160,6 +161,7 @@ pred fold-map i:term, i:A, o:term, o:A.
 :name "fold-map:start"
 fold-map X A Y A :- name X, !, X = Y, !. % avoid loading "fold-map x A x A" at binders
 fold-map (global _ as C) A C A :- !.
+fold-map (pglobal _ _ as C) A C A :- !.
 fold-map (sort _ as C) A C A :- !.
 fold-map (fun N T F) A (fun N T1 F1) A2 :- !,
   fold-map T A T1 A1, pi x\ fold-map (F x) A1 (F1 x) A2.
@@ -192,6 +194,30 @@ fold-map-arity (arity T) A (arity T1) A1 :- fold-map T A T1 A1.
 % The arguments are the same of coq.env.indt plus an an extra one being
 % the output (of type indt-decl).
 
+pred coq.upoly-decl->attribute i:any, o:prop.
+coq.upoly-decl->attribute (upoly-decl A B C D) (@udecl! A B C D).
+coq.upoly-decl->attribute (upoly-decl-cumul A B C D) (@udecl-cumul! A B C D).
+
+pred coq.upoly-decl.complete-constraints i:upoly-decl, o:upoly-decl.
+coq.upoly-decl.complete-constraints (upoly-decl VS LV CS LC) (upoly-decl VS LV CS1 LC) :- std.do! [
+  std.map VS coq.univ.variable.constraints ExtraL,
+  std.flatten ExtraL Extra,
+  std.filter Extra (c\not(std.mem CS c)) New,
+  std.append CS New CS1,
+].
+pred coq.upoly-decl-cumul.complete-constraints i:upoly-decl-cumul, o:upoly-decl-cumul.
+coq.upoly-decl-cumul.complete-constraints (upoly-decl-cumul VS LV CS LC) (upoly-decl-cumul VS LV CS1 LC) :- std.do! [
+  std.map VS coq.upoly-decl-cumul.complete-constraints.aux ExtraL,
+  std.flatten ExtraL Extra,
+  std.filter Extra (c\not(std.mem CS c)) New,
+  std.append CS New CS1,
+].
+coq.upoly-decl-cumul.complete-constraints.aux (auto V) CS :- coq.univ.variable.constraints V CS.
+coq.upoly-decl-cumul.complete-constraints.aux (covariant V) CS :- coq.univ.variable.constraints V CS.
+coq.upoly-decl-cumul.complete-constraints.aux (invariant V) CS :- coq.univ.variable.constraints V CS.
+coq.upoly-decl-cumul.complete-constraints.aux (irrelevant V) CS :- coq.univ.variable.constraints V CS.
+
+
 pred coq.build-indt-decl
   i:(pair inductive id), i:bool, i:int, i:int, i:term, i:list (pair constructor id), i:list term, o:indt-decl.
 
@@ -205,8 +231,8 @@ coq.build-indt-decl-aux (pr GR I) IsInd NUPno 0 Ty Kns KtysNu Params (inductive
   std.map KtysNu (k\coq.term->arity k NUPno) Ktys,
   rev Params ParamsR,
   (pi i\ Sub i = [ % we factor uniform parameters
-     (pi x l\ copy (app[global (indt GR)|l]) (app[i|x]):- !, appendR ParamsR x l),
-     (copy (global (indt GR)) i :- !) ]),
+    (pi x l\ copy (app[global (indt GR)|l]) (app[i|x]):- !, appendR ParamsR x l),
+    (copy (global (indt GR)) i :- !) ]),
   pi i\
     map2 Kns Ktys (gr_name\ ty\ res\
       sigma tmp name\
@@ -266,7 +292,7 @@ coq.rename-indt-decl.aux RP _ RK (constructor ID A) (constructor ID1 A1) :-
 % Lifts coq.typecheck to inductive declarations
 pred coq.typecheck-indt-decl.heuristic-var-type i:term, o:diagnostic.
 coq.typecheck-indt-decl.heuristic-var-type (uvar _ _ as X) D :- !,
-  coq.univ.new [] U, coq.unify-eq X (sort (typ U)) D.
+  coq.univ.new U, coq.unify-eq X (sort (typ U)) D.
 coq.typecheck-indt-decl.heuristic-var-type _ ok.
 
 pred coq.typecheck-indt-decl i:indt-decl, o:diagnostic.
@@ -292,7 +318,7 @@ coq.typecheck-indt-decl-c I S (constructor _ID Arity) Diag :- coq.arity->term Ar
   coq.typecheck-ty T KS,
   coq.typecheck-indt-decl-c.unify-arrow-tgt I 0 S T,
   lift-ok (coq.arity->sort S IS) "",
-  lift-ok (if (IS = typ U1, KS = typ U2) (coq.univ.leq U2 U1) true) "constructor universe too large"
+  lift-ok (coq.sort.leq KS IS) "constructor universe too large"
 ].
 
 pred coq.typecheck-indt-decl-c.unify-arrow-tgt i:term, i:int, i:term, i:term, o:diagnostic.
@@ -331,11 +357,11 @@ coq.elaborate-indt-decl-skeleton (record ID A IDK FDecl) (record ID A1 IDK FDecl
   d\ @pi-parameter ID A1 i\ coq.elaborate-indt-decl-skeleton-fields U FDecl FDecl1 d
 ].
 
-pred coq.elaborate-indt-decl-skeleton-fields i:universe, i:record-decl, o:record-decl, o:diagnostic.
+pred coq.elaborate-indt-decl-skeleton-fields i:sort, i:record-decl, o:record-decl, o:diagnostic.
 coq.elaborate-indt-decl-skeleton-fields _ end-record end-record ok.
 coq.elaborate-indt-decl-skeleton-fields U (field Att ID A Fields) (field Att ID A1 Fields1) Diag :- do-ok! Diag [
   coq.elaborate-ty-skeleton A UA A1,
-  lift-ok (if (U = typ U1, UA = typ U2) (coq.univ.leq U2 U1) true) "constructor universe too large",
+  lift-ok (coq.sort.leq UA U) "constructor universe too large",
   d\ @pi-parameter ID A1 p\
        coq.elaborate-indt-decl-skeleton-fields U (Fields p) (Fields1 p) d
 ].
@@ -345,7 +371,7 @@ coq.elaborate-indt-decl-skeleton-c I SA (constructor ID Arity) (constructor ID A
   coq.elaborate-arity-skeleton Arity KS Arity1,
   coq.typecheck-indt-decl-c.unify-arity I 0 SA Arity1,
   lift-ok (coq.arity->sort {coq.arity->term SA} IS) "",
-  lift-ok (if (IS = typ U1, KS = typ U2) (coq.univ.leq U2 U1) true) "constructor universe too large"
+  lift-ok (coq.sort.leq KS IS) "constructor universe too large"
 ].
 
 pred coq.typecheck-indt-decl-c.unify-arity i:term, i:int, i:arity, i:arity, o:diagnostic.
@@ -360,7 +386,7 @@ coq.typecheck-indt-decl-c.unify-arity I PNO (arity A) (arity C) D :-
   coq.typecheck-indt-decl-c.unify-arrow-tgt I PNO A C D.
 
 % Lifts coq.elaborate-skeleton to arity
-pred coq.elaborate-arity-skeleton i:arity, o:universe, o:arity, o:diagnostic.
+pred coq.elaborate-arity-skeleton i:arity, o:sort, o:arity, o:diagnostic.
 coq.elaborate-arity-skeleton (parameter ID Imp T A) U (parameter ID Imp T1 A1) Diag :- do-ok! Diag [
   coq.elaborate-ty-skeleton T _ T1, % parameters don't count
   d\ @pi-parameter ID T1 i\ coq.elaborate-arity-skeleton (A i) U (A1 i) d
@@ -383,7 +409,7 @@ coq.term->arity (prod Name S T) N (parameter ID explicit S R) :-
   @pi-decl Name S x\ coq.term->arity (T x) M (R x).
 
 % extracts the sort at the end of an arity
-pred coq.arity->sort i:term, o:universe.
+pred coq.arity->sort i:term, o:sort.
 coq.arity->sort (prod N S X) Y :- !, @pi-decl N S x\ coq.arity->sort (X x) Y.
 coq.arity->sort (sort X) X :- !.
 :name "arity->sort:fail"
@@ -433,6 +459,7 @@ coq.any-implicit? L :- std.exists L (x\not(x = explicit)).
 % extract gref from terms that happen to have one
 pred coq.term->gref i:term, o:gref.
 coq.term->gref (global GR) GR :- !.
+coq.term->gref (pglobal GR _) GR :- !.
 coq.term->gref (app [Hd|_]) GR :- !, coq.term->gref Hd GR.
 coq.term->gref (let _ _ T x\x) GR :- !, coq.term->gref T GR.
 :name "term->gref:fail"
@@ -440,7 +467,7 @@ coq.term->gref Term _ :-
   fatal-error-w-data "term->gref: input has no global reference" Term.
 
 pred coq.fresh-type o:term.
-coq.fresh-type (sort (typ U)) :- coq.univ.new [] U.
+coq.fresh-type (sort (typ U)) :- coq.univ.new U.
 
 % Map the term under a spine of fun nodes
 pred coq.map-under-fun i:term,
@@ -475,7 +502,7 @@ pred coq.build-match
   i:(term -> term -> list term -> list term -> term -> prop),
   o:term. % match T (.. MkRty) [ .. MkBranch K1, .. MkBranch K2, ..]
 coq.build-match T Tty RtyF BranchF (match T Rty Bs) :-
-  whd Tty [] (global (indt GR)) Args,
+  whd Tty [] (global (indt GR)) Args, !,
   coq.env.indt GR _ Lno _ Arity Kn Kt,
   take Lno Args LArgs,
   coq.mk-app (global (indt GR)) LArgs IndtLArgs,
@@ -488,6 +515,20 @@ coq.build-match T Tty RtyF BranchF (match T Rty Bs) :-
   map KtArgsNorm coq.prod->fun KtArgsLam,
   map Kn (k\ coq.mk-app (global (indc k)) LArgs) KnArgs,
   map2 KnArgs KtArgsLam (k\t\coq.map-under-fun t (BranchF k)) Bs.
+coq.build-match T Tty RtyF BranchF (match T Rty Bs) :-
+  whd Tty [] (pglobal (indt GR) I) Args,
+  @uinstance! I => coq.env.indt GR _ Lno _ Arity Kn Kt,
+  take Lno Args LArgs,
+  coq.mk-app (pglobal (indt GR) I) LArgs IndtLArgs,
+  % Rty
+  coq.subst-prod LArgs Arity ArityArgs,
+  coq.bind-ind-arity-no-let IndtLArgs ArityArgs RtyF Rty,
+  % Bs
+  map Kt (coq.subst-prod LArgs) KtArgs,
+  map KtArgs hd-beta-zeta-reduce KtArgsNorm,
+  map KtArgsNorm coq.prod->fun KtArgsLam,
+  map Kn (k\ coq.mk-app (pglobal (indc k) I) LArgs) KnArgs,
+  map2 KnArgs KtArgsLam (k\t\coq.map-under-fun t (BranchF k)) Bs.
 
 % XXX the list of arguments are often needed in reverse order
 pred coq.bind-ind-arity % calls K under (fun Arity (x : Ity Arity) =>..)
diff --git a/elpi/elpi-reduction.elpi b/elpi/elpi-reduction.elpi
index 8932e9895..a0f8ed7e1 100644
--- a/elpi/elpi-reduction.elpi
+++ b/elpi/elpi-reduction.elpi
@@ -33,7 +33,8 @@ whd (fun N T F) [B|C] X XC :- !,
   (pi x\ def x N T B => cache x BN_ => whd (F x) C (F1 x) (C1 x)), X = F1 B, XC = C1 B.
 whd (let N T B F) C X XC :- !,
   (pi x\ def x N T B => cache x BN_ => whd (F x) C (F1 x) (C1 x)), X = F1 B, XC = C1 B.
-whd (global (const GR)) C X XC :- unfold GR C D DC, !, whd D DC X XC.
+whd (global (const GR)) C X XC :- unfold GR none C D DC, !, whd D DC X XC.
+whd (pglobal (const GR) I) C X XC :- unfold GR (some I) C D DC, !, whd D DC X XC.
 whd (primitive (proj _ N)) [A|C] X XC :- whd-indc A _ KA, !,
   whd {proj-red KA N C} X XC.
 whd (global (const GR) as HD) C X XC :- coq.env.primitive? GR, !,
@@ -76,11 +77,13 @@ fix-red F Fix LA GR KA RA X XC :-
   hd-beta {coq.mk-app (F Fix) ArgsWRedRecNo} [] X XC.
 
 pred unfold % delta (global constants) + hd-beta
-  i:constant,    % name
-  i:stack,   % args
-  o:term,     % body
-  o:stack.    % args after hd-beta
-unfold GR A BO BOC :- coq.env.const GR (some B) _, hd-beta B A BO BOC.
+  i:constant,             % name
+  i:option univ-instance, % universe instance if the constant is universe polymorphic
+  i:stack,                % args
+  o:term,                 % body
+  o:stack.                % args after hd-beta
+unfold GR none A BO BOC :- coq.env.const GR (some B) _, hd-beta B A BO BOC.
+unfold GR (some I) A BO BOC :- @uinstance! I => coq.env.const GR (some B) _, hd-beta B A BO BOC.
 
 % ensures its first argument is the whd of the second
 pred cache i:term, o:term.
diff --git a/elpi/elpi_elaborator.elpi b/elpi/elpi_elaborator.elpi
index e11355db6..c12ef58ce 100644
--- a/elpi/elpi_elaborator.elpi
+++ b/elpi/elpi_elaborator.elpi
@@ -61,30 +61,35 @@ swap ff F A B :- F A B.
 
 unif (sort prop) [] (sort (uvar as Y)) [] _ _ :- !, Y = prop.
 unif X [] (sort (uvar as Y)) [] M U :- !,
-  coq.univ.new [] Lvl,
+  coq.univ.new Lvl,
   Y = typ Lvl,
   unif X [] (sort Y) [] M U.
 unif (sort (uvar as X)) [] Y [] M U :- !,
-  coq.univ.new [] Lvl,
+  coq.univ.new Lvl,
   X = typ Lvl,
   unif (sort X) [] Y [] M U.
 
-unif (sort (typ S1)) [] (sort (typ S2)) [] M eq  :- !, swap M coq.univ.eq S1 S2.
-unif (sort (typ S1)) [] (sort (typ S2)) [] M leq :- !, swap M coq.univ.leq S1 S2.
-unif (sort (typ _)) [] (sort prop) [] ff _ :- !, fail.
-unif (sort prop) [] (sort (typ _)) [] ff eq :- !, fail.
-unif (sort prop) [] (sort (typ _)) [] ff leq :- !.
-unif (sort prop) [] (sort prop) [] ff eq :- !.
+unif (sort S1) [] (sort S2) [] M eq  :- !, swap M coq.sort.eq S1 S2.
+unif (sort S1) [] (sort S2) [] M leq :- !, swap M coq.sort.leq S1 S2.
 
-unif (sort X) [] (sort X) [] ff _ :- !.
 unif (primitive X) [] (primitive X) [] ff _ :- !.
 
 unif (global (indt GR1)) C (global (indt GR2)) D _ _ :- !, GR1 = GR2, unify-ctxs C D.
 unif (global (indc GR1)) C (global (indc GR2)) D _ _ :- !, GR1 = GR2, unify-ctxs C D.
+unif (pglobal (indt GR1) I1) C (pglobal (indt GR2) I2) D _ eq :- !,
+  GR1 = GR2,
+  coq.univ-instance.unify-eq (indt GR1) I1 I2 ok,
+  unify-ctxs C D.
+unif (pglobal (indt GR1) I1) C (pglobal (indt GR2) I2) D _ leq :- !,
+  GR1 = GR2,
+  coq.univ-instance.unify-leq (indt GR1) I1 I2 ok,
+  unify-ctxs C D.
 
 % fast path for stuck term on the right
 unif X C (global (indt _) as T) D ff U :- !, unif T D {whd X C} tt U. % TODO:1
 unif X C (global (indc _) as T) D ff U :- !, unif T D {whd X C} tt U. % TODO:1
+unif X C (pglobal (indt _) _ as T) D ff U :- !, unif T D {whd X C} tt U. % TODO:1
+unif X C (pglobal (indc _) _ as T) D ff U :- !, unif T D {whd X C} tt U. % TODO:1
 
 % congruence rules TODO: is the of assumption really needed?
 unif (fun N T1 F1) [] (fun M T2 F2) [] _ _ :- !, ignore-failure! (N = M),
@@ -106,10 +111,17 @@ unif (let N T1 B1 F1) C1 (let M T2 B2 F2) C2 _ _ :- ignore-failure! (N = M),
   (@pi-def N T1 B1 x\ unify (F1 x) (F2 x) eq),
   unify-ctxs C1 C2, !.
 unif (global (const GR)) C (global (const GR)) D _ _ :- unify-ctxs C D, !.
+unif (pglobal (const GR) I1) C (pglobal (const GR) I2) D _ eq :-
+  coq.univ-instance.unify-eq (const GR) I1 I2 ok,
+  unify-ctxs C D, !.
+unif (pglobal (const GR) I1) C (pglobal (const GR) I2) D _ leq :-
+  coq.univ-instance.unify-leq (const GR) I1 I2 ok,
+  unify-ctxs C D, !.
 unif X C T D _ _ :- name X, name T, X = T, unify-ctxs C D.
 
 % 1 step reduction  TODO:1
-unif (global (const GR)) C T D M U :- unfold GR C X1 C1, !, unif X1 C1 T D M U.
+unif (global (const GR)) C T D M U :- unfold GR none C X1 C1, !, unif X1 C1 T D M U.
+unif (pglobal (const GR) I) C T D M U :- unfold GR (some I) C X1 C1, !, unif X1 C1 T D M U.
 unif (let N TB B F) C1 T C2 M U :- !,
   @pi-def N TB B x\ unif {hd-beta (F x) C1} T C2 M U.
 unif (match A _ L) C T D M U :- whd-indc A GR KA, !,
@@ -151,6 +163,7 @@ unify-list-eq L1 L2 :- unify-list L1 L2.
 % We use a keyd discipline, i.e. we only bind terms with a rigid head
 pred key i:term.
 key (global _) :- !.
+key (pglobal _ _) :- !.
 key C :- name C, !.
 key (primitive _) :- !.
 
@@ -174,6 +187,7 @@ pred bind i:term, o:term.
 bind X Y :- name X, X = Y, !.
 bind X Y :- name X, def X _ _ T, !, bind T Y.
 bind (global _ as C) C :- !.
+bind (pglobal _ _ as C) C :- !.
 bind (sort _ as C) C :- !.
 bind (fix N Rno Ty F) (fix N Rno Ty1 F1) :- !,
   bind Ty Ty1, pi x\ decl x N Ty => bind (F x) (F1 x).
@@ -289,16 +303,11 @@ of (fix N Rno Ty BoF) ResTy (fix N Rno RTy ResBoF) :-
   unify-leq RTy ResTy,
   pi f\ decl f N RTy => of (BoF f) ResTy (ResBoF f).
  
-of (sort prop) (sort (typ U)) (sort prop) :-
-  if (var U) (coq.univ.new [] U) true.
-of (sort (typ T) as X) (sort S) X :-       % XXX TODO: unif
-  coq.univ.sup T T+1, 
-  if (var S) (S = typ T+1)
-     (if (S = prop) false
-         (S = typ U, coq.univ.leq T+1 U)).
-of (sort V) T X :- var V, coq.univ.new [] U, V = typ U, of (sort V) T X.
+of (sort S) (sort S1) (sort S) :- coq.sort.sup S S1.
 
 of (global GR as X) T X :- coq.env.typeof GR T1, unify-leq T1 T.
+of (pglobal GR I as X) T X :-
+  @uinstance! I => coq.env.typeof GR T1, unify-leq T1 T.
 
 of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:elpi.uint63 }} T.
 of (primitive (float64 _) as X) T X :- unify-leq {{ lib:elpi.float64 }} T.
@@ -363,24 +372,13 @@ mk-bty Rty Lno T Ki AppRtyNorm :-
   split-at Lno Args LArgs RArgs,
   coq.mk-app Rty {append RArgs [{coq.mk-app (global (indc Ki)) {append LArgs RArgs}}]} AppRty,
   hd-beta-zeta-reduce AppRty AppRtyNorm.
+mk-bty Rty Lno T Ki AppRtyNorm :-
+  coq.safe-dest-app T (pglobal (indt _) I) Args,
+  split-at Lno Args LArgs RArgs,
+  coq.mk-app Rty {append RArgs [{coq.mk-app (pglobal (indc Ki) I) {append LArgs RArgs}}]} AppRty,
+  hd-beta-zeta-reduce AppRty AppRtyNorm.
 
 % PTS sorts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-pred pts i:universe, i:universe, o:universe.
-
-pts  prop     prop     prop.
-pts (typ U)   prop     prop :- if (var U) (coq.univ.new [] U) true.
-pts (typ T1) (typ T2) (typ M) :- coq.univ.pts-triple T1 T2 M.
-pts  prop    (typ T2) (typ T2).
-
-pts (uvar    as X) (prop  as Y) R :- coq.univ.new [] U, X = typ U, pts X Y R.
-pts (prop  as X) (uvar    as Y) R :- coq.univ.new [] U, Y = typ U, pts X X R.
-pts (uvar    as X) (typ _ as Y) R :- coq.univ.new [] U, X = typ U, pts X Y R.
-pts (typ _ as X) (uvar    as Y) R :- coq.univ.new [] U, Y = typ U, pts X Y R.
-pts (uvar    as X) (uvar    as Y) R :- not(var R), R = prop, !,
-  X = prop, Y = prop.
-pts (uvar    as X) (uvar    as Y) R :- var R, !,
-  coq.univ.new [] U, X = typ U,
-  coq.univ.new [] V, Y = typ V,
-  pts X Y R.
-% vim:set ft=lprolog spelllang=:
+pred pts i:sort, i:sort, o:sort.
+pts  X Y U :- coq.sort.pts-triple X Y U.
diff --git a/examples/tutorial_coq_elpi_HOAS.v b/examples/tutorial_coq_elpi_HOAS.v
index c7fd91485..7e7c3216f 100644
--- a/examples/tutorial_coq_elpi_HOAS.v
+++ b/examples/tutorial_coq_elpi_HOAS.v
@@ -258,10 +258,10 @@ impose constraints.
 
 Elpi Query lp:{{
 
-  coq.univ.sup U U1,
+  coq.sort.sup U U1,
   coq.say U "<" U1,
   % This constraint can't be allowed in the store!
-  not(coq.univ.leq U1 U)
+  not(coq.sort.leq U1 U)
 
 }}.
 
diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 956d1b511..834e39688 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -54,6 +54,247 @@ let in_coq_name ~depth t =
   | E.UnifVar _ -> Name.Anonymous
   | _ -> err Pp.(str"Not a name: " ++ str (API.RawPp.Debug.show_term t))
 
+(* engine prologue, to break ciclicity *)
+
+type coq_engine = {
+   global_env : Environ.env;
+   sigma : Evd.evar_map; (* includes universe constraints *)
+}
+let pre_engine : coq_engine S.component option ref = ref None
+
+(* universes *)
+
+module UnivOrd = struct
+  type t = Univ.Universe.t
+  let compare = Univ.Universe.compare
+  let show x = Pp.string_of_ppcmds (Univ.Universe.pr x)
+  let pp fmt x = Format.fprintf fmt "%s" (show x)
+end
+module UnivSet = U.Set.Make(UnivOrd)
+module UnivMap = U.Map.Make(UnivOrd)
+module UnivLevelOrd = struct
+  type t = Univ.Level.t
+  let compare = Univ.Level.compare
+  let show x = Pp.string_of_ppcmds (Univ.Level.pr x)
+  let pp fmt x = Format.fprintf fmt "%s" (show x)
+end
+module UnivLevelSet = U.Set.Make(UnivLevelOrd)
+module UnivLevelMap = U.Map.Make(UnivLevelOrd)
+
+(* map from Elpi evars and Coq's universe levels *)
+module UM = F.Map(struct
+  type t = Univ.Universe.t
+  let compare = Univ.Universe.compare
+  let show x = Pp.string_of_ppcmds @@ Univ.Universe.pr x
+  let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Universe.pr x)
+end)
+
+let um = S.declare ~name:"coq-elpi:evar-univ-map"
+  ~pp:UM.pp ~init:(fun () -> UM.empty) ~start:(fun x -> x)
+
+
+let constraint_leq u1 u2 =
+  let open UnivProblem in
+  ULe (u1, u2)
+
+let constraint_eq u1 u2 =
+  let open UnivProblem in
+  ULe (u1, u2)
+
+let add_constraints state c = S.update (Option.get !pre_engine) state (fun ({ sigma } as x) ->
+  { x with sigma = Evd.add_universe_constraints sigma c })
+    
+let add_universe_constraint state c =
+  let open UnivProblem in
+  try add_constraints state (Set.singleton c)
+  with
+  | UGraph.UniverseInconsistency p ->
+      Feedback.msg_debug
+        (UGraph.explain_universe_inconsistency
+            UnivNames.(pr_with_global_universes empty_binders) p);
+      raise API.BuiltInPredicate.No_clause
+  | Evd.UniversesDiffer | UState.UniversesDiffer ->
+      Feedback.msg_debug Pp.(str"UniversesDiffer");
+      raise API.BuiltInPredicate.No_clause
+
+let unames = ref 0
+let new_univ_level_variable state =
+  S.update_return (Option.get !pre_engine) state (fun ({ sigma } as e) ->
+    (* ~name: really mean the universe level is a binder as in Definition f@{x} *)
+    let sigma, v = Evd.new_univ_level_variable ?name:None UState.univ_rigid sigma in
+    let u = Univ.Universe.make v in
+    (*
+    let sigma = Evd.add_universe_constraints sigma
+        (UnivProblem.Set.singleton (UnivProblem.ULe (Sorts.type1,Sorts.sort_of_univ u))) in
+*)
+    { e with sigma }, (v, u))
+
+(* We patch data_of_cdata by forcing all output universes that
+ * are unification variables to be a Coq universe variable, so that
+ * we can always call Coq's API *)
+let isuniv, univout, (univ : Univ.Universe.t API.Conversion.t) =
+  let { CD.cin = univin; isc = isuniv; cout = univout }, univ_to_be_patched = CD.declare {
+    CD.name = "univ";
+    doc = "universe level (algebraic: max, +1, univ-variable)";
+    pp = (fun fmt x ->
+      let s = Pp.string_of_ppcmds (Univ.Universe.pr x) in
+      Format.fprintf fmt "«%s»" s);
+    compare = Univ.Universe.compare;
+    hash = Univ.Universe.hash;
+    hconsed = false;
+    constants = [];
+  } in
+  (* turn UVars into fresh universes *)
+  isuniv, univout, { univ_to_be_patched with
+  API.Conversion.readback = begin fun ~depth state t ->
+    match E.look ~depth t with
+    | E.UnifVar (b,args) ->
+       let m = S.get um state in
+       begin try
+         let u = UM.host b m in
+         state, u, []
+       with Not_found ->
+         let state, (_,u) = new_univ_level_variable state in
+         let state = S.update um state (UM.add b u) in
+         state, u, [ API.Conversion.Unify(E.mkUnifVar b ~args state,univin u) ]
+       end
+    | _ -> univ_to_be_patched.API.Conversion.readback ~depth state t
+  end
+}
+
+let sort =
+  let open API.AlgebraicData in  declare {
+  ty = API.Conversion.TyName "sort";
+  doc = "Sorts (kinds of types)";
+  pp = (fun fmt -> function
+    | Sorts.Type _ -> Format.fprintf fmt "Type"
+    | Sorts.Set -> Format.fprintf fmt "Set"
+    | Sorts.Prop -> Format.fprintf fmt "Prop"
+    | Sorts.SProp -> Format.fprintf fmt "SProp");
+  constructors = [
+    K("prop","impredicative sort of propositions",N,
+      B Sorts.prop,
+      M (fun ~ok ~ko -> function Sorts.Prop -> ok | _ -> ko ()));
+    K("sprop","impredicative sort of propositions with definitional proof irrelevance",N,
+      B Sorts.sprop,
+      M (fun ~ok ~ko -> function Sorts.SProp -> ok | _ -> ko ()));
+    K("typ","predicative sort of data (carries a universe level)",A(univ,N),
+      B (fun x -> Sorts.sort_of_univ x),
+      M (fun ~ok ~ko -> function
+        | Sorts.Type x -> ok x
+        | Sorts.Set -> ok Univ.Universe.type0
+        | _ -> ko ()));
+    K("uvar","",A(API.FlexibleData.uvar,N),
+      BS (fun (k,_) state ->
+        let m = S.get um state in
+        try
+          let u = UM.host k m in
+          state, Sorts.sort_of_univ u
+        with Not_found ->
+          let state, (_,u) = new_univ_level_variable state in
+          let state = S.update um state (UM.add k u) in
+          state, Sorts.sort_of_univ u),
+      M (fun ~ok ~ko _ -> ko ()));
+  ]
+} |> API.ContextualConversion.(!<)
+
+
+let universe_level_variable =
+  let { CD.cin = levelin }, universe_level_variable_to_patch = CD.declare {
+    CD.name = "univ-variable";
+    doc = "universe level variable";
+    pp = (fun fmt x ->
+      let s = Pp.string_of_ppcmds (Univ.Level.pr x) in
+      Format.fprintf fmt "«%s»" s);
+    compare = Univ.Level.compare;
+    hash = Univ.Level.hash;
+    hconsed = false;
+    constants = [];
+  } in
+  { universe_level_variable_to_patch with
+  API.Conversion.readback = begin fun ~depth state t ->
+    match E.look ~depth t with
+    | E.UnifVar (b,args) ->
+       let m = S.get um state in
+       begin try
+         let u = UM.host b m in
+         state, Option.get @@ Univ.Universe.level u, []
+       with Not_found ->
+         let state, (l,u) = new_univ_level_variable state in
+         let state = S.update um state (UM.add b u) in
+         state, l, [ API.Conversion.Unify(E.mkUnifVar b ~args state,levelin l) ]
+       end
+    | _ -> universe_level_variable_to_patch.API.Conversion.readback ~depth state t
+  end
+}
+
+let universe_constraint : Univ.univ_constraint API.Conversion.t =
+  let open API.Conversion in let open API.AlgebraicData in declare {
+  ty = TyName "univ-constraint";
+  doc = "Constraint between two universes level variables";
+  pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
+  constructors = [
+    K("lt","",A(universe_level_variable,A(universe_level_variable,N)),
+      B (fun u1 u2 -> (u1,Univ.Lt,u2)),
+      M (fun ~ok ~ko -> function (l1,Univ.Lt,l2) -> ok l1 l2 | _ -> ko ()));
+    K("le","",A(universe_level_variable,A(universe_level_variable,N)),
+      B (fun u1 u2 -> (u1,Univ.Le,u2)),
+      M (fun ~ok ~ko -> function (l1,Univ.Le,l2) -> ok l1 l2 | _ -> ko ()));
+    K("eq","",A(universe_level_variable,A(universe_level_variable,N)),
+      B (fun u1 u2 -> (u1,Univ.Eq,u2)),
+      M (fun ~ok ~ko -> function (l1,Univ.Eq,l2) -> ok l1 l2 | _ -> ko ()))
+  ]
+} |> API.ContextualConversion.(!<)
+
+let universe_variance : (Univ.Level.t * Univ.Variance.t option) API.Conversion.t =
+  let open API.Conversion in let open API.AlgebraicData in declare {
+  ty = TyName "univ-variance";
+  doc = "Variance of a universe level variable";
+  pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
+  constructors = [
+    K("auto","",A(universe_level_variable,N),
+      B (fun u -> u,None),
+      M (fun ~ok ~ko -> function (u,None) -> ok u | _ -> ko ()));
+    K("covariant","",A(universe_level_variable,N),
+      B (fun u -> u,Some Univ.Variance.Covariant),
+      M (fun ~ok ~ko -> function (u,Some Univ.Variance.Covariant) -> ok u | _ -> ko ()));
+    K("invariant","",A(universe_level_variable,N),
+      B (fun u -> u,Some Univ.Variance.Invariant),
+      M (fun ~ok ~ko -> function (u,Some Univ.Variance.Invariant) -> ok u | _ -> ko ()));
+    K("irrelevant","",A(universe_level_variable,N),
+      B (fun u -> u,Some Univ.Variance.Invariant),
+      M (fun ~ok ~ko -> function (u,Some Univ.Variance.Irrelevant) -> ok u | _ -> ko ()));
+  ]
+} |> API.ContextualConversion.(!<)
+
+type universe_decl = (Univ.Level.t list * bool) * (Univ.Constraints.t * bool)
+let universe_decl : universe_decl API.Conversion.t =
+  let open API.Conversion in let open API.BuiltInData in let open API.AlgebraicData in let open Elpi.Builtin in declare {
+  ty = TyName "upoly-decl";
+  doc = "Constraints for a non-cumulative declaration. Boolean tt means loose (e.g. the '+' in f@{u v + | u < v +})";
+  pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
+  constructors = [
+    K("upoly-decl","",A(list universe_level_variable,A(bool,A(list universe_constraint,A(bool,N)))),
+     B (fun x sx y sy-> (x,sx),(Univ.Constraints.of_list  y,sy)),
+     M (fun ~ok ~ko:_ ((x,sx),(y,sy)) -> ok x sx (Univ.Constraints.elements y) sy))
+  ]
+} |> API.ContextualConversion.(!<)
+
+type universe_decl_cumul = ((Univ.Level.t * Univ.Variance.t option) list  * bool) * (Univ.Constraints.t * bool)
+let universe_decl_cumul : universe_decl_cumul API.Conversion.t =
+  let open API.Conversion in let open API.BuiltInData in let open API.AlgebraicData in let open Elpi.Builtin in declare {
+  ty = TyName "upoly-decl-cumul";
+  doc = "Constraints for a cumulative declaration. Boolean tt means loose (e.g. the '+' in f@{u v + | u < v +})";
+  pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
+  constructors = [
+    K("upoly-decl-cumul","",A(list universe_variance,A(bool,A(list universe_constraint,A(bool,N)))),
+     B (fun x sx y sy -> ((x,sx),(Univ.Constraints.of_list y,sy))),
+     M (fun ~ok ~ko:_ ((x,sx),(y,sy)) -> ok x sx (Univ.Constraints.elements y) sy))
+  ]
+} |> API.ContextualConversion.(!<)
+
+
+
 (* All in one data structure to represent the Coq context and its link with
    the elpi one:
    - section is not part of the elpi context, but Coq's evars are applied
@@ -72,6 +313,17 @@ type hole_mapping =
   | Verbatim   (* 1:1 correspondence between UVar and Evar *)
   | Heuristic  (* new UVar outside Llam is pruned before being linked to Evar *)
   | Implicit   (* No link, UVar is intepreted as a "hole" constant *)
+type uinstanceoption =
+  | NoInstance
+    (* the elpi command involved has to generate a fresh instance *)
+  | ConcreteInstance of Univ.Instance.t
+    (* a concrete instance was provided, the command will use it *)
+  | VarInstance of (F.Elpi.t * E.term list * inv_rel_key)
+    (* a variable was provided, the command will compute the instance to unify with it *)
+type universe_decl_option =
+  | NotUniversePolymorphic
+  | Cumulative of universe_decl_cumul
+  | NonCumulative of universe_decl
 type options = {
   hoas_holes : hole_mapping option;
   local : bool option;
@@ -83,6 +335,8 @@ type options = {
   pplevel : Constrexpr.entry_relative_level;
   using : string option;
   inline : Declaremods.inline;
+  uinstance : uinstanceoption;
+  universe_decl : universe_decl_option;
 }
 
 let default_options = {
@@ -96,6 +350,8 @@ let default_options = {
   pplevel = Constrexpr.LevelSome;
   using = None;
   inline = Declaremods.NoInline;
+  uinstance = NoInstance;
+  universe_decl = NotUniversePolymorphic
 }
 
 type 'a coq_context = {
@@ -148,22 +404,6 @@ let in_coq_fresh_annot_id ~depth ~coq_ctx dbl t =
   let get_name = function Name.Name x -> x | Name.Anonymous -> assert false in
   Context.make_annot (in_coq_fresh ~id_only:true ~depth ~coq_ctx dbl t |> get_name) Sorts.Relevant
 
-(* universes *)
-let univin, isuniv, univout, univ_to_be_patched =
-  let { CD.cin; isc; cout }, univ = CD.declare {
-    CD.name = "univ";
-    doc = "universe level";
-    pp = (fun fmt x ->
-      let s = Pp.string_of_ppcmds (Sorts.debug_print x) in
-      Format.fprintf fmt "«%s»" s);
-    compare = Sorts.compare;
-    hash = Sorts.hash;
-    hconsed = false;
-    constants = [];
-  } in
-  cin, isc, cout, univ
-;;
-
 let unspec2opt = function Elpi.Builtin.Given x -> Some x | Elpi.Builtin.Unspec -> None
 let opt2unspec = function Some x -> Elpi.Builtin.Given x | None -> Elpi.Builtin.Unspec
 
@@ -221,6 +461,22 @@ let ({ CD.isc = isconstant; cout = constantout; cin = constantin },constant),
   }
 ;;
 
+let uinstancein, _isuinstance, _uinstanceout, uinstance =
+  let { CD.cin; isc; cout }, uinstance = CD.declare {
+    CD.name = "univ-instance";
+    doc = "Universes level instance for a universe-polymoprhic constant";
+    pp = (fun fmt x ->
+      let s = Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr x) in
+      Format.fprintf fmt "«%s»" s);
+    compare = (fun x y ->
+      CArray.compare Univ.Level.compare (Univ.Instance.to_array x) (Univ.Instance.to_array y));
+    hash = Univ.Instance.hash;
+    hconsed = false;
+    constants = [];
+  } in
+  cin, isc, cout, uinstance
+;;
+
 let collect_term_variables ~depth t =
   let rec aux ~depth acc t =
     match E.look ~depth t with
@@ -296,6 +552,7 @@ module GRMap = U.Map.Make(GROrd)
 module GRSet = U.Set.Make(GROrd)
 
 let globalc  = E.Constants.declare_global_symbol "global"
+let pglobalc  = E.Constants.declare_global_symbol "pglobal"
 
 module GrefCache = Hashtbl.Make(struct
   type t = GlobRef.t
@@ -304,7 +561,29 @@ module GrefCache = Hashtbl.Make(struct
 end)
 let cache = GrefCache.create 13
 
+let assert_in_coq_gref_consistent ~poly gr =
+  match Global.is_polymorphic gr, poly with
+  | true, true -> ()
+  | false, false -> ()
+  | true, false ->
+    U.type_error Printf.(sprintf "Universe polymorphic gref %s used with the 'global' term constructor" (GROrd.show gr))
+  | false, true ->
+    U.type_error Printf.(sprintf "Non universe polymorphic gref %s used with the 'pglobal' term constructor" (GROrd.show gr))
+;;
+
+let assert_in_elpi_gref_consistent ~poly gr =
+  match Global.is_polymorphic gr, poly with
+  | true, true -> ()
+  | false, false -> ()
+  | true, false ->
+    U.anomaly Printf.(sprintf "Universe polymorphic gref %s used with the 'global' term constructor" (GROrd.show gr))
+  | false, true ->
+    U.anomaly Printf.(sprintf "Non universe polymorphic gref %s used with the 'pglobal' term constructor" (GROrd.show gr))
+;;
+
+
 let in_elpi_gr ~depth s r =
+  assert_in_elpi_gref_consistent ~poly:false r;
   try
     GrefCache.find cache r
   with Not_found ->
@@ -314,9 +593,24 @@ let in_elpi_gr ~depth s r =
     GrefCache.add cache r x;
     x
 
+let in_elpi_poly_gr ~depth s r i =
+  assert_in_elpi_gref_consistent ~poly:true r;
+  let open API.Conversion in
+  let s, t, gl = gref.embed ~depth s r in
+  assert (gl = []);
+  E.mkApp pglobalc t [i]
+
+let in_elpi_poly_gr_instance ~depth s r i =
+  assert_in_elpi_gref_consistent ~poly:true r;
+  let open API.Conversion in
+  let s, i, gl = uinstance.embed ~depth s i in
+  assert (gl = []);
+  in_elpi_poly_gr ~depth s r i
+
 let in_coq_gref ~depth ~origin ~failsafe s t =
   try
     let s, t, gls = gref.API.Conversion.readback ~depth s t in
+    assert_in_coq_gref_consistent ~poly:false t;
     assert(gls = []);
     s, t
   with API.Conversion.TypeErr _ ->
@@ -456,12 +750,6 @@ let command_mode =
 
 module CoqEngine_HOAS : sig 
 
-  type coq_engine  = {
-   global_env : Environ.env;
-   sigma : Evd.evar_map; (* includes universe constraints *)
-
-  }
-
   val show_coq_engine : ?with_univs:bool -> coq_engine -> string
 
   val engine : coq_engine S.component
@@ -471,11 +759,6 @@ module CoqEngine_HOAS : sig
 
 end = struct
 
- type coq_engine = {
-   global_env : Environ.env [@printer (fun _ _ -> ())];
-   sigma : Evd.evar_map [@printer (fun fmt m ->
-     Format.fprintf fmt "%a" Pp.pp_with (Termops.pr_evar_map None (Global.env()) m))];
- }
  let pp_coq_engine ?with_univs fmt { sigma } =
    Format.fprintf fmt "%a" Pp.pp_with (Termops.pr_evar_map ?with_univs None (Global.env()) sigma)
 
@@ -500,7 +783,7 @@ let show_coq_engine ?with_univs e = Format.asprintf "%a" (pp_coq_engine ?with_un
      ~pp:pp_coq_engine ~init ~start:(fun _ -> init())
 
 end
-
+let () = pre_engine := Some CoqEngine_HOAS.engine
 open CoqEngine_HOAS
 
 (* Bidirectional mapping between Elpi's UVars and Coq's Evars.
@@ -593,98 +876,43 @@ let section_ids env =
       (fun acc x -> Context.Named.Declaration.get_id x :: acc)
       ~init:[] named_ctx
 
-(* map from Elpi evars and Coq's universe levels *)
-module UM = F.Map(struct
-  type t = Sorts.t
-  let compare = Sorts.compare
-  let show x = Pp.string_of_ppcmds @@ Sorts.debug_print x
-  let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Sorts.debug_print x)
-end)
-
-let um = S.declare ~name:"coq-elpi:evar-univ-map"
-  ~pp:UM.pp ~init:(fun () -> UM.empty) ~start:(fun x -> x)
-
-let new_univ state =
-  S.update_return engine state (fun ({ sigma } as x) ->
-    let sigma, v = Evd.new_univ_level_variable UState.UnivRigid sigma in
-    let u = Sorts.sort_of_univ @@ Univ.Universe.make v in
-    let sigma = Evd.add_universe_constraints sigma
-        (UnivProblem.Set.singleton (UnivProblem.ULe (Sorts.type1,u))) in
-    { x with sigma }, u)
+let sortc  = E.Constants.declare_global_symbol "sort"
+let typc   = E.Constants.declare_global_symbol "typ"  
+
+let force_level_of_universe state u =
+  match Univ.Universe.level u with
+  | Some lvl -> state, lvl, u, Sorts.sort_of_univ u
+  | None ->
+      let state, (l,v) = new_univ_level_variable state in
+      let w = Sorts.sort_of_univ v in
+      add_universe_constraint state (constraint_eq (Sorts.sort_of_univ u) w), l, v, w
+
+let purge_algebraic_univs_sort state s =
+  let sigma = (S.get engine state).sigma in
+  match EConstr.ESorts.kind sigma s with
+  | Sorts.Type u ->
+      let state, _, _, s = force_level_of_universe state u in
+      state, s
+  | x -> state, x
 
-(* We patch data_of_cdata by forcing all output universes that
- * are unification variables to be a Coq universe variable, so that
- * we can always call Coq's API *)
-let univ =
-  (* turn UVars into fresh universes *)
-  { univ_to_be_patched with
-  API.Conversion.readback = begin fun ~depth state t ->
-    match E.look ~depth t with
-    | E.UnifVar (b,args) ->
-       let m = S.get um state in
-       begin try
-         let u = UM.host b m in
-         state, u, []
-       with Not_found ->
-         let state, u = new_univ state in
-         let state = S.update um state (UM.add b u) in
-         state, u, [ API.Conversion.Unify(E.mkUnifVar b ~args state,univin u) ]
-       end
-    | _ -> univ_to_be_patched.API.Conversion.readback ~depth state t
-  end
-}
+let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []
 
-let universe =
-  let open API.AlgebraicData in  declare {
-  ty = API.Conversion.TyName "universe";
-  doc = "Universes (for the sort term former)";
-  pp = (fun fmt -> function
-    | Sorts.Type _ -> Format.fprintf fmt "Type"
-    | Sorts.Set -> Format.fprintf fmt "Set"
-    | Sorts.Prop -> Format.fprintf fmt "Prop"
-    | Sorts.SProp -> Format.fprintf fmt "SProp");
-  constructors = [
-    K("prop","impredicative sort of propositions",N,
-      B Sorts.prop,
-      M (fun ~ok ~ko -> function Sorts.Prop -> ok | _ -> ko ()));
-    K("sprop","impredicative sort of propositions with definitional proof irrelevance",N,
-      B Sorts.sprop,
-      M (fun ~ok ~ko -> function Sorts.SProp -> ok | _ -> ko ()));
-    K("typ","predicative sort of data (carries a level)",A(univ,N),
-      B (fun x -> x),
-      M (fun ~ok ~ko -> function
-        | Sorts.Type _ as x -> ok x
-        | Sorts.Set -> ok Sorts.set
-        | _ -> ko ()));
-  ]
-} |> API.ContextualConversion.(!<)
+let sort = { sort with API.Conversion.embed = (fun ~depth state s ->
+  let state, s = purge_algebraic_univs_sort state (EConstr.ESorts.make s) in
+  sort.API.Conversion.embed ~depth state s) }
 
-let sortc  = E.Constants.declare_global_symbol "sort"
-let propc  = E.Constants.declare_global_symbol "prop"
-let spropc = E.Constants.declare_global_symbol "sprop"
-let typc   = E.Constants.declare_global_symbol "typ"
-
-let in_elpi_sort s =
-  E.mkApp
-    sortc
-    (match s with
-    | Sorts.SProp -> E.mkGlobal spropc
-    | Sorts.Prop -> E.mkGlobal propc
-    | Sorts.Set -> E.mkApp typc (univin Sorts.set) []
-    | Sorts.Type _ as u -> E.mkApp typc (univin u) [])
-    []
+let in_elpi_sort ~depth state s =
+  let state, s, gl = sort.API.Conversion.embed ~depth state s in
+  assert(gl=[]);
+  state, E.mkApp sortc s []
 
-let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []
 
 (* ********************************* }}} ********************************** *)
 
 (* {{{ HOAS : EConstr.t -> elpi ******************************************* *)
 
-let check_univ_inst univ_inst =
-  if not (Univ.Instance.is_empty univ_inst) then
-    nYI "HOAS universe polymorphism"
-    
 let get_sigma s = (S.get engine s).sigma
+let update_sigma s f = (S.update engine s (fun e -> { e with sigma = f e.sigma }))
 let get_global_env s = (S.get engine s).global_env
 
 let declare_evc = E.Constants.declare_global_symbol "declare-evar"
@@ -807,6 +1035,17 @@ let get_options ~depth hyps state =
       let _, b, _ = Elpi.Builtin.(pair (unspec fst) (unspec snd)).API.Conversion.readback ~depth state t in
       Some b
     with Not_found -> None in
+  let get_uinstance_option name =
+    match API.Data.StrMap.find_opt name map with
+    | Some (t, depth) when t <> E.mkDiscard -> begin
+      match E.look ~depth t with
+      | E.UnifVar (head, args) -> VarInstance (head, args, depth)
+      | _ ->
+        let _, i, gl = uinstance.Elpi.API.Conversion.readback ~depth state t in
+        assert (gl = []);
+        ConcreteInstance i
+    end
+    | _ -> NoInstance in
   let empty2none = function Some "" -> None | x -> x in
   let deprecation = function
     | None -> None
@@ -814,6 +1053,19 @@ let get_options ~depth hyps state =
         let since = unspec2opt since |> empty2none in
         let note = unspec2opt note |> empty2none in
         Some { Deprecation.since; note } in
+  let get_universe_decl () =
+    match API.Data.StrMap.find_opt "coq:udecl-cumul" map, API.Data.StrMap.find_opt "coq:udecl" map with
+    | None, None -> NotUniversePolymorphic
+    | Some _, Some _ -> err Pp.(str"Conflicting attributes: @udecl! and @udecl-cumul! (or @univpoly! and @univpoly-cumul!)")
+    | Some (t,depth), None ->
+        let _, ud, gl = universe_decl_cumul.Elpi.API.Conversion.readback ~depth state t in
+        assert (gl = []);
+        Cumulative ud
+    | None, Some (t,depth) ->
+      let _, ud, gl = universe_decl.Elpi.API.Conversion.readback ~depth state t in
+      assert (gl = []);
+      NonCumulative ud
+    in
   {
     hoas_holes =
       begin match get_bool_option "HOAS:holes" with
@@ -829,6 +1081,8 @@ let get_options ~depth hyps state =
     pplevel = pplevel @@ get_int_option "coq:pplevel";
     using = get_string_option "coq:using";
     inline = get_module_inline_option "coq:inline";
+    uinstance = get_uinstance_option "coq:uinstance";
+    universe_decl = get_universe_decl ();
   }
 
 let mk_coq_context ~options state =
@@ -968,7 +1222,7 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
          let args = CList.firstn (List.length args - coq_ctx.section_len) args in
          let state, args = CList.fold_left_map (aux ~depth env) state args in
          state, E.mkUnifVar elpi_uvk ~args:(List.rev args) state
-    | C.Sort s -> state, in_elpi_sort (EC.ESorts.kind sigma s)
+    | C.Sort s -> in_elpi_sort ~depth state (EC.ESorts.kind sigma s)
     | C.Cast (t,_,ty0) ->
          let state, t = aux ~depth env state t in
          let state, ty = aux ~depth env state ty0 in
@@ -995,15 +1249,18 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
          let state, hd = aux ~depth env state hd in
          let state, args = CArray.fold_left_map (aux ~depth env) state args in
          state, in_elpi_app ~depth hd args
+    | C.Const(c,i) when Global.is_polymorphic (G.ConstRef c) ->
+         state, in_elpi_poly_gr_instance ~depth state (G.ConstRef c) (EC.EInstance.kind sigma i)
     | C.Const(c,i) ->
-         check_univ_inst (EC.EInstance.kind sigma i);
-         let ref = G.ConstRef c in
-         state, in_elpi_gr ~depth state ref
-    | C.Ind(ind,i) ->
-         check_univ_inst (EC.EInstance.kind sigma i);
+         state, in_elpi_gr ~depth state (G.ConstRef c)
+    | C.Ind (ind, i) when Global.is_polymorphic (G.IndRef ind) ->
+         state, in_elpi_poly_gr_instance ~depth state (G.IndRef ind) (EC.EInstance.kind sigma i)
+    | C.Ind (ind, i) ->
          state, in_elpi_gr ~depth state (G.IndRef ind)
-    | C.Construct(construct,i) ->
-         check_univ_inst (EC.EInstance.kind sigma i);
+    | C.Construct (construct, i) when Global.is_polymorphic (G.ConstructRef construct) ->
+         let gref = G.ConstructRef construct in
+         state, in_elpi_poly_gr_instance ~depth state gref (EC.EInstance.kind sigma i)
+    | C.Construct (construct, i) ->
          state, in_elpi_gr ~depth state (G.ConstructRef construct)
     | C.Case(ci, u, pms, rt, iv, t, bs) ->
          let (_, rt, _, t, bs) = EConstr.expand_case env sigma (ci, u, pms, rt, iv, t, bs) in
@@ -1142,21 +1399,43 @@ let () = E.set_extra_goals_postprocessing (fun l state ->
 
 (* {{{ HOAS : elpi -> Constr.t * Evd.evar_map ***************************** *)
 
-let add_constraints state c = S.update engine state (fun ({ sigma } as x) ->
-  { x with sigma = Evd.add_universe_constraints sigma c })
-
-
-let type_of_global state r = S.update_return engine state (fun x ->
-  let ty, ctx = Typeops.type_of_global_in_context x.global_env r in
-  let inst, ctx = UnivGen.fresh_instance_from ctx None in
-  let ty = Vars.subst_instance_constr inst ty in
-  let sigma = Evd.merge_context_set Evd.univ_rigid x.sigma ctx in
-  { x with sigma }, EConstr.of_constr ty)
-
-let body_of_constant state c = S.update_return engine state (fun x ->
-  match Global.body_of_constant_body Library.indirect_accessor (Environ.lookup_constant c x.global_env) with
+let poly_ctx_size_of_gref env gr =
+  let open Names.GlobRef in
+  match gr with
+  | VarRef _ -> 0
+  | ConstRef c ->
+    let cb = Environ.lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    Univ.AbstractContext.size univs
+  | IndRef ind ->
+    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    Univ.AbstractContext.size univs
+  | ConstructRef cstr ->
+    let (mib,_ as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    Univ.AbstractContext.size univs
+
+let mk_global state gr inst_opt = S.update_return engine state (fun x ->
+  match inst_opt with
+  | None ->
+      let sigma, t = EConstr.fresh_global x.global_env x.sigma gr in
+      let _, i = EConstr.destRef sigma t in
+      { x with sigma }, (t, Some (EConstr.EInstance.kind sigma i))
+  | Some ui ->
+      if poly_ctx_size_of_gref x.global_env gr != Univ.Instance.length ui then
+        U.type_error "xxx TODO";
+      let i = EConstr.EInstance.make ui in
+      x, (EConstr.mkRef (gr,i), None)
+) |> (fun (x,(y,z)) -> x,y,z)
+
+let body_of_constant state c inst_opt = S.update_return engine state (fun x ->
+  match
+    Global.body_of_constant_body Library.indirect_accessor (Environ.lookup_constant c x.global_env)
+  with
   | Some (bo, priv, ctx) ->
-     let inst, ctx = UnivGen.fresh_instance_from ctx None in
+     let inst, ctx = UnivGen.fresh_instance_from ctx inst_opt in
      let bo = Vars.subst_instance_constr inst bo in
      let sigma = Evd.merge_context_set Evd.univ_rigid x.sigma ctx in
      let sigma = match priv with
@@ -1165,17 +1444,22 @@ let body_of_constant state c = S.update_return engine state (fun x ->
       let ctx = Util.on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst inst)) ctx in
       Evd.merge_context_set Evd.univ_rigid sigma ctx
      in
-     { x with sigma }, Some (EConstr.of_constr bo)
-  | None -> x, None)
+     { x with sigma }, (Some (EConstr.of_constr bo), Some inst)
+  | None -> x, (None, None)) |> (fun (x,(y,z)) -> x,y,z)
 
 let evar_arity k state =
   let info = Evd.find (S.get engine state).sigma k in
   let filtered_hyps = Evd.evar_filtered_hyps info in
   List.length (Environ.named_context_of_val filtered_hyps)
 
-let minimize_universes state =
+(* This is random: u < v /\ u <= FOO.123 /\ FOO.123 <= u ===>
+                   u < FOO.123
+   even if u is a binder, and FOO.123 is not.
+   Hence this is disabled. *)
+let minimize_universes state = state (*
   S.update engine state (fun ({ sigma } as x) ->
     { x with sigma = Evd.minimize_universes sigma })
+*)
 
 let is_sort ~depth x =
   match E.look ~depth x with
@@ -1294,6 +1578,56 @@ let analyze_scope ~depth coq_ctx args =
    in
       aux E.Constants.Set.empty [] [] false true args
 
+module UIM = F.Map(struct
+  type t = Univ.Instance.t
+  let compare i1 i2 =
+    CArray.compare Univ.Level.compare (Univ.Instance.to_array i1) (Univ.Instance.to_array i2)
+  let show x = Pp.string_of_ppcmds @@ Univ.Instance.pr Univ.Level.pr x
+  let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Instance.pr Univ.Level.pr x)
+end)
+    
+let uim = S.declare ~name:"coq-elpi:evar-univ-instance-map"
+  ~pp:UIM.pp ~init:(fun () -> UIM.empty) ~start:(fun x -> x)
+    
+let in_coq_poly_gref ~depth ~origin ~failsafe s t i =
+  let open API.Conversion in
+  let uinstance_readback s i t =
+    match E.look ~depth i with
+    | E.UnifVar (b, args) ->
+      let m = S.get uim s in
+      begin try
+        let u = UIM.host b m in
+        s, u, []
+      with Not_found ->
+        let u, ctx = UnivGen.fresh_global_instance (get_global_env s) t in
+        let s = update_sigma s (fun sigma -> Evd.merge_context_set UState.univ_flexible_alg sigma ctx) in
+        let u =
+          match C.kind u with
+          | C.Const (_, u) -> u
+          | C.Ind (_, u) -> u
+          | C.Construct (_, u) -> u
+          | _ -> assert false
+        in
+        let s = S.update uim s (UIM.add b u) in
+        s, u, [API.Conversion.Unify (E.mkUnifVar b ~args s,uinstancein u)]
+      end
+    | _ -> uinstance.readback ~depth s i
+  in
+  try
+    let s, t, gls1 = gref.readback ~depth s t in
+    assert_in_coq_gref_consistent ~poly:true t;
+    let s, i, gls2 = uinstance_readback s i t in
+    assert (gls1 = []);
+    s, t, i, gls2
+  with API.Conversion.TypeErr _ ->
+    if failsafe then
+      s, Coqlib.lib_ref "elpi.unknown_gref", Univ.Instance.empty, []
+    else
+      let open Pp in
+      err ?loc:None @@
+        str "The term " ++ str (pp2string (P.term depth) origin) ++
+        str " cannot be represented in Coq since its gref or univ-instance part is illformed"
+
 let rec of_elpi_ctx ~calldepth syntactic_constraints depth dbl2ctx state initial_coq_ctx =
 
   let aux coq_ctx depth state t =
@@ -1346,7 +1680,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
   debug Pp.(fun () -> str"lp2term@" ++ int depth ++ str":" ++ str(pp2string (P.term depth) t));
   match E.look ~depth t with
   | E.App(s,p,[]) when sortc == s ->
-      let state, u, gsl = universe.API.Conversion.readback ~depth state p in
+      let state, u, gsl = sort.API.Conversion.readback ~depth state p in
       state, EC.mkSort u, gsl
  (* constants *)
   | E.App(c,d,[]) when globalc == c ->
@@ -1357,6 +1691,15 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
      | G.ConstructRef x -> state, EC.mkConstruct x, []
      | G.IndRef x -> state, EC.mkInd x, []
      end
+  | E.App(c,d,[i]) when pglobalc == c ->
+    let state, gr, i, gls =
+      in_coq_poly_gref ~depth ~origin:t ~failsafe:coq_ctx.options.failsafe state d i in
+    begin match gr with
+    | G.VarRef x -> assert false (* TODO: nice error *)
+    | G.ConstRef x -> state, EC.mkConstU (x, EC.EInstance.make i), gls
+    | G.ConstructRef x -> state, EC.mkConstructU (x, EC.EInstance.make i), gls
+    | G.IndRef x -> state, EC.mkIndU (x, EC.EInstance.make i), gls
+    end
  (* binders *)
   | E.App(c,name,[s;t]) when lamc == c || prodc == c ->
       let name = in_coq_fresh_annot_name ~depth ~coq_ctx depth name in
@@ -2178,13 +2521,125 @@ let readback_arity ~depth coq_ctx constraints state t =
     aux_arity coq_ctx ~depth [] [] state [] t
 ;;
 
+
+let inference_nonuniform_params_off =
+  CWarnings.create
+    ~name:"elpi.unsupported-nonuniform-parameters-inference"
+    ~category:"elpi" Pp.(fun () ->
+      strbrk"Inference of non-uniform parameters is not available in Elpi, please use the explicit | mark in the inductive declaration or Set Uniform Inductive Parameters")
+      
+module Hack_Name_Univ_Level = struct
+type uinfo = {
+  uname : Id.t option;
+  uloc : Loc.t option;
+}
+      
+type t =
+  { names : UnivNames.universe_binders * uinfo Univ.Level.Map.t; (** Printing/location information *)
+    local : unit;
+    seff_univs : unit;
+    univ_variables : unit;
+    univ_algebraic : unit;
+    universes : unit;
+    universes_lbound : unit;
+    initial_universes : unit;
+    minim_extra : unit;
+  }
+let unseal_ustate_t : UState.t -> t =
+  assert(let _,v,_ = coq_version_parser Coq_config.version in v = 16); (* remove this hack on coq 8.17 *)
+  Obj.magic
+
+let seal_ustate_t : t -> UState.t =
+  assert(let _,v,_ = coq_version_parser Coq_config.version in v = 16); (* remove this hack on coq 8.17 *)
+  Obj.magic
+  
+let hack_name_level l (t : UState.t) : UState.t * Id.t =
+  let t = unseal_ustate_t t in
+  let (names, names_rev) = t.names in
+  incr unames;
+  let s = Id.of_string ("u" ^ string_of_int !unames) in
+  if Names.Id.Map.mem s names
+  then err Pp.(str "Universe " ++ Names.Id.print s ++ str" already bound.");
+  seal_ustate_t { t with names = (Names.Id.Map.add s l names, Univ.Level.Map.add l { uname = Some s; uloc = None } names_rev) },
+  s
+
+let hack_restrict (s : Univ.Level.Set.t) (t : UState.t) : UState.t =
+  let t = unseal_ustate_t t in
+  let (names, names_rev) = t.names in
+  let names = Names.Id.Map.filter (fun _ l -> Univ.Level.Set.mem l s) names in
+  let names_rev = Univ.Level.Map.filter (fun l _ -> Univ.Level.Set.mem l s) names_rev in
+  let t = { t with names = (names, names_rev) } in
+  seal_ustate_t t
+
+end
+
+let restricted_sigma_of s state =
+  let sigma = get_sigma state in
+  let ustate = Evd.evar_universe_context sigma in
+  let ustate = Hack_Name_Univ_Level.hack_restrict s ustate in
+  let sigma = Evd.set_universe_context sigma ustate in
+  let sigma = Evd.restrict_universe_context sigma s in
+  sigma
+
+let universes_of_term state t =
+  let sigma = get_sigma state in
+  EConstr.universes_of_constr sigma t
+
+let universes_of_udecl state ({ UState.univdecl_instance ; univdecl_constraints } : UState.universe_decl) =
+  let sigma = get_sigma state in
+  let used1 = List.map (fun x -> Evd.universe_of_name sigma x.CAst.v ) univdecl_instance in
+  let used2 = List.map (fun (x,_,y) -> [x;y]) (Univ.Constraints.elements univdecl_constraints) in
+  let used = List.fold_right Univ.Level.Set.add used1 Univ.Level.Set.empty in
+  let used = List.fold_right Univ.Level.Set.add (List.flatten used2) used in
+  used
+
+let name_universe_level state l =
+  S.update_return engine state (fun e ->
+    let ustate = Evd.evar_universe_context e.sigma in
+    match UState.id_of_level ustate l with
+    | Some id -> e, id
+    | None ->
+        let ustate, id = Hack_Name_Univ_Level.hack_name_level l ustate in
+        let sigma = Evd.set_universe_context e.sigma ustate in
+        { e with sigma }, id
+  )
+
+let poly_cumul_udecl_variance_of_options state options =
+  let sigma = get_sigma state in
+  let universe_name state (u, v) =
+    match UState.id_of_level (Evd.evar_universe_context sigma) u with
+    | None ->
+        let state, id = name_universe_level state u in
+        state, (CAst.make id, v)
+    | Some id -> state, (CAst.make id, v) in
+  match options.universe_decl with
+  | NotUniversePolymorphic -> state, false, false, UState.default_univ_decl, [| |]
+  | Cumulative ((univ_lvlt_var,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) ->
+    let state, univdecl_instance_variance = CList.fold_left_map universe_name state univ_lvlt_var in
+    let univdecl_instance, variance = List.split univdecl_instance_variance in
+    let open UState in
+    state, true, true,
+    { univdecl_extensible_instance;
+      univdecl_extensible_constraints;
+      univdecl_constraints;
+      univdecl_instance},
+    Array.of_list variance
+  | NonCumulative((univ_lvlt,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) ->
+    let state, univdecl_instance_variance = CList.fold_left_map (fun s x -> universe_name s (x,None)) state univ_lvlt in
+    let univdecl_instance, variance = List.split univdecl_instance_variance in
+    let open UState in
+    state, true, false,
+    { univdecl_extensible_instance;
+      univdecl_extensible_constraints;
+      univdecl_constraints;
+      univdecl_instance},
+      Array.of_list variance
+
 let lp2inductive_entry ~depth coq_ctx constraints state t =
 
   let lp2constr coq_ctx ~depth state t =
     lp2constr constraints coq_ctx ~depth state t in
 
-  let open Entries in
-
   let check_consistency_and_drop_nuparams sigma nuparams name params arity =
     let eq_param x y =
       Name.equal
@@ -2239,6 +2694,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
      *  Params, Ind, NuParams |- ktys
      * To
      *  Ind, Params, NuParams |- ktys
+     * This latter context is called, later, env_ar_params
      *)
     let ktypes = ktypes |> List.map (fun t ->
       let subst = CList.init (nupno + paramno + 1) (fun i ->
@@ -2254,12 +2710,78 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
       EC.Vars.substl subst t
     ) in
 
-    let params = nuparams @ params in
+    let state, (mind, ubinders, uctx) =
+      let private_ind = false in
+      let state, poly, cumulative, udecl, variances =
+        poly_cumul_udecl_variance_of_options state coq_ctx.options in
+      let the_type =
+        let open Context.Rel.Declaration in
+        LocalAssum(Context.nameR itname, EConstr.it_mkProd_or_LetIn arity (nuparams @ params)) in
+      let env_ar_params = (Global.env ()) |> EC.push_rel the_type |> EC.push_rel_context (nuparams @ params) in
+      let arityconcl =
+        match Reductionops.sort_of_arity env_ar_params sigma arity with
+        | exception Reduction.NotArity -> None
+        | s -> Some (false,s) in
+
+    (* restruction to used universes *)
+    let state = minimize_universes state in
+    let used =
+      List.fold_left (fun acc t ->
+          Univ.Level.Set.union acc
+            (universes_of_term state t))
+        (universes_of_term state arity) ktypes in
+    let used =
+      let open Context.Rel.Declaration in
+      List.fold_left (fun acc -> function
+        | (LocalDef(_,t,b)) ->
+          Univ.Level.Set.union acc
+           (Univ.Level.Set.union
+            (universes_of_term state t)
+            (universes_of_term state b))
+        | (LocalAssum(_,t)) ->
+          Univ.Level.Set.union acc
+            (universes_of_term state t))
+        used (nuparams @ params) in
+    let sigma = restricted_sigma_of used state in
+
+    Feedback.msg_info Pp.(str"after restriction:" ++
+      let uc = Evd.evar_universe_context sigma in
+      let uc = Termops.pr_evar_universe_context uc in
+      uc);
+
+      state, ComInductive.interp_mutual_inductive_constr
+        ~sigma
+        ~template:(Some false)
+        ~udecl
+        ~variances
+        ~ctx_params:(nuparams @ params)
+        ~indnames:[itname]
+        ~arities:[arity]
+        ~arityconcl:[arityconcl]
+        ~constructors:[knames, List.map (EC.to_constr sigma) ktypes]
+        ~env_ar_params
+        ~cumulative
+        ~poly
+        ~private_ind
+        ~finite:finiteness
+      in
+    let mind = { mind with
+      Entries.mind_entry_record =
+        if finiteness = Declarations.BiFinite then
+          if coq_ctx.options.primitive = Some true then Some (Some [|Names.Id.of_string "record"|]) (* primitive record *)
+          else Some None (* regular record *)
+        else None } (* not a record *) in
     let i_impls = impls @ nuimpls in
 
+    state, mind, uctx, ubinders, i_impls, kimpls, List.(concat (rev gls_rev))
+
+    (*
+      
+      let params = nuparams @ params in
     debug Pp.(fun () ->
         str"Inductive declaration with sigma:" ++ cut() ++
         Termops.pr_evar_map None (Global.env()) sigma);
+
     let state = minimize_universes state in
     let sigma = get_sigma state in
     let ktypes = List.map (EC.to_constr sigma) ktypes in
@@ -2272,23 +2794,26 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
     let used =
       List.fold_left (fun acc t ->
           Univ.Level.Set.union acc
-            (EConstr.universes_of_constr sigma (EConstr.of_constr t)))
-        (EConstr.universes_of_constr sigma (EConstr.of_constr arity)) ktypes in
+            (universes_of_term state (EConstr.of_constr t)))
+        (universes_of_term state (EConstr.of_constr arity)) ktypes in
     let used =
       List.fold_left (fun acc -> function
         | (LocalDef(_,t,b)) ->
           Univ.Level.Set.union acc
            (Univ.Level.Set.union
-            (EConstr.universes_of_constr sigma (EConstr.of_constr t))
-            (EConstr.universes_of_constr sigma (EConstr.of_constr b)))
+            (universes_of_term state (EConstr.of_constr t))
+            (universes_of_term state (EConstr.of_constr b)))
         | (LocalAssum(_,t)) ->
           Univ.Level.Set.union acc
-            (EConstr.universes_of_constr sigma (EConstr.of_constr t)))
+            (universes_of_term state (EConstr.of_constr t)))
         used params in
     let sigma = Evd.restrict_universe_context sigma used in
     debug Pp.(fun () ->
         str"Inductive declaration with restricted sigma:" ++ cut() ++
         Termops.pr_evar_map None (Global.env()) sigma);
+
+    let state = S.update engine state (fun e -> { e with sigma}) in
+    let ubinders, mind_entry_universes, mind_entry_variance, uctx = handle_univ_decl state coq_ctx.options in
     let oe = {
       mind_entry_typename = itname;
       mind_entry_arity = arity;
@@ -2304,9 +2829,10 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
       mind_entry_finite = finiteness;
       mind_entry_params = params;
       mind_entry_inds = [oe];
-      mind_entry_universes = Monomorphic_ind_entry;
-      mind_entry_variance = None;
-      mind_entry_private = None; }, Evd.universe_context_set sigma, i_impls, kimpls, List.(concat (rev gls_rev))
+      mind_entry_universes;
+      mind_entry_variance;
+      mind_entry_private = None; }, uctx, ubinders, i_impls, kimpls, List.(concat (rev gls_rev))
+      *)
   in
 
   let rec aux_fields depth state ind fields =
@@ -2351,10 +2877,10 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
         begin match E.look ~depth ks with
         | E.Lam t ->
             let ks = U.lp_list_to_list ~depth:(depth+1) t in
-            let state, idecl, ctx, i_impls, ks_impls, gl2 =
+            let state, idecl, uctx, ubinders, i_impls, ks_impls, gl2 =
               aux_construtors (push_coq_ctx_local depth e coq_ctx) ~depth:(depth+1) (params,List.rev impls) (nuparams, List.rev nuimpls) arity iname fin
                 state ks in
-            state, (idecl, ctx, None, [i_impls, ks_impls]), List.(concat (rev (gl2 :: gl1 :: extra)))
+            state, (idecl, uctx, ubinders, None, [i_impls, ks_impls]), List.(concat (rev (gl2 :: gl1 :: extra)))
         | _ -> err Pp.(str"lambda expected: "  ++
                  str (pp2string P.(term depth) ks))
         end
@@ -2375,11 +2901,11 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
         let ind = E.mkConst depth in
         let state, fields_names_coercions, kty = aux_fields (depth+1) state ind fields in
         let k = [E.mkApp constructorc kn [in_elpi_arity kty]] in
-        let state, idecl, ctx, i_impls, ks_impls, gl2 =
+        let state, idecl, uctx, ubinders, i_impls, ks_impls, gl2 =
           aux_construtors (push_coq_ctx_local depth e coq_ctx) ~depth:(depth+1) (params,impls) ([],[]) arity iname Declarations.BiFinite
             state k in
         let primitive = coq_ctx.options.primitive = Some true in
-        state, (idecl, ctx, Some (primitive,fields_names_coercions), [i_impls, ks_impls]), List.(concat (rev (gl2 :: gl1 :: extra)))
+        state, (idecl, uctx, ubinders, Some (primitive,fields_names_coercions), [i_impls, ks_impls]), List.(concat (rev (gl2 :: gl1 :: extra)))
       | _ -> err Pp.(str"id expected, got: "++
                  str (pp2string P.(term depth) kn))
       end
@@ -2463,6 +2989,33 @@ let under_coq2elpi_relctx ~calldepth state (ctx : 'a ctx_entry list) ~coq_ctx ~m
     state, t, !gls
 ;;
 
+
+let type_of_global state r inst_opt = API.State.update_return engine state (fun x ->
+  let ty, ctx = Typeops.type_of_global_in_context x.global_env r in
+  let inst, ctx = UnivGen.fresh_instance_from ctx inst_opt in
+  let ty = Vars.subst_instance_constr inst ty in
+  let sigma = Evd.merge_context_set Evd.univ_rigid x.sigma ctx in
+  { x with sigma }, (EConstr.of_constr ty, inst))
+
+
+let compute_with_uinstance ~depth options state f x inst_opt =
+  match options.uinstance with
+  | NoInstance ->
+    let state, r, i = f state x inst_opt in
+    state, r, i, []
+  | ConcreteInstance i ->
+    let state, r, i = f state x (Option.append inst_opt (Some i)) in
+    state, r, i, []
+  | VarInstance (v_head, v_args, v_depth) ->
+    let state, r, i = f state x inst_opt in
+    match i with
+    | None -> state, r, None, []
+    | Some uinst ->
+      let v' = U.move ~from:v_depth ~to_:depth (E.mkUnifVar v_head ~args:v_args state) in
+      let state, lp_uinst, extra_goals = uinstance.API.Conversion.embed ~depth state uinst in
+      state, r, Some uinst, API.Conversion.Unify (v', lp_uinst) :: extra_goals
+    
+
 let embed_arity ~depth coq_ctx state (relctx,ty) =
   let calldepth = depth in
   under_coq2elpi_relctx ~calldepth ~coq_ctx state relctx
@@ -2543,7 +3096,10 @@ let drop_nparams_from_ctx n ctx =
   let ctx, _ = CList.chop (List.length ctx - n) ctx in
   ctx
 
-let inductive_decl2lp ~depth coq_ctx constraints state (mutind,(mind,ind),(i_impls,k_impls)) =
+let ideclc = E.Constants.declare_global_symbol "indt-decl"
+let uideclc = E.Constants.declare_global_symbol "upoly-indt-decl"
+
+let inductive_decl2lp ~depth coq_ctx constraints state (mutind,uinst,(mind,ind),(i_impls,k_impls)) =
   let { Declarations.mind_params_ctxt;
         mind_finite = kind;
         mind_nparams = allparamsno;
@@ -2557,7 +3113,8 @@ let inductive_decl2lp ~depth coq_ctx constraints state (mutind,(mind,ind),(i_imp
   let { Declarations.mind_consnames = constructor_names;
         mind_typename = id;
         mind_nf_lc = constructor_types } = ind in
-  let arity_w_params = Inductive.type_of_inductive ((mind,ind),Univ.Instance.empty) in
+  let constructor_types = constructor_types |> Array.map (fun (ctx,ty) -> Vars.subst_instance_context uinst ctx, Vars.subst_instance_constr uinst ty) in
+  let arity_w_params = Inductive.type_of_inductive ((mind,ind),uinst) in
   let sigma = get_sigma state in
   let drop_nparams_from_term n x =
     let x = EConstr.of_constr x in
@@ -2612,14 +3169,28 @@ let inductive_decl2lp ~depth coq_ctx constraints state (mutind,(mind,ind),(i_imp
   let ind = { params; decl } in
   hoas_ind2lp ~depth coq_ctx state ind
 ;;
+       
+let upoly_decl_of ~depth state ~loose_udecl mie =
+  let open Entries in
+  match mie.mind_entry_universes with
+  | Template_ind_entry _ -> nYI "template polymorphic inductives"
+  | Polymorphic_ind_entry uc ->
+      let vars = Univ.Instance.to_array @@ Univ.UContext.instance uc in
+      let state, vars = CArray.fold_left_map (fun s l -> fst (name_universe_level s l), l) state vars in
+      let csts = Univ.UContext.constraints uc in
+      begin match mie.mind_entry_variance with
+      | None ->
+          let state, up, gls = universe_decl.API.Conversion.embed ~depth state ((Array.to_list vars,loose_udecl),(csts,loose_udecl)) in
+          state, (fun i -> E.mkApp uideclc i [up]), gls
+      | Some variance ->
+          assert(Array.length variance = Array.length vars);
+          let uv = Array.map2 (fun x y -> (x,y)) vars variance |> Array.to_list in
+          let state, up, gls = universe_decl_cumul.API.Conversion.embed ~depth state ((uv,loose_udecl),(csts,loose_udecl)) in
+          state, (fun i -> E.mkApp uideclc i [up]), gls
+      end
+  | Monomorphic_ind_entry -> state, (fun i -> E.mkApp ideclc i []), []
 
-let inference_nonuniform_params_off =
-  CWarnings.create
-    ~name:"elpi.unsupported-nonuniform-parameters-inference"
-    ~category:"elpi" Pp.(fun () ->
-      strbrk"Inference of non-uniform parameters is not available in Elpi, please use the explicit | mark in the inductive declaration or Set Uniform Inductive Parameters")
-
-let inductive_entry2lp ~depth coq_ctx constraints state e =
+let inductive_entry2lp ~depth coq_ctx constraints state ~loose_udecl e =
   let open ComInductive.Mind_decl in
   let open Entries in
   let { mie; nuparams; univ_binders; implicits; uctx } = e in
@@ -2631,17 +3202,16 @@ let inductive_entry2lp ~depth coq_ctx constraints state e =
   let ind = match mie.mind_entry_inds with
   | [ x ] -> x
   | _ -> nYI "mutual inductives" in
-  if not (Names.Id.Map.is_empty univ_binders) then nYI "universe binders inductives";
   let indno = 1 in
   let state = 
     S.update engine state (fun e ->
       { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma uctx}) in
   let state = match mie.mind_entry_universes with
-    | Template_ind_entry ctx ->
-      S.update engine state (fun e ->
-        { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma ctx})
+    | Template_ind_entry _ -> nYI "template polymorphic inductives"
     | Monomorphic_ind_entry -> state
-    | Polymorphic_ind_entry _ -> nYI "univpoly ind" in
+    | Polymorphic_ind_entry cs -> S.update engine state (fun e ->
+        { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma (Univ.ContextSet.of_context cs) }) (* ???? *) in
+  let state, upoly_decl_of, upoly_decl_gls = upoly_decl_of ~depth state ~loose_udecl mie in
   let allparams = mie.mind_entry_params in
   let allparams = Vars.lift_rel_context indno allparams in
   let kind = mie.mind_entry_finite in
@@ -2652,7 +3222,9 @@ let inductive_entry2lp ~depth coq_ctx constraints state e =
         let open Declarations in
         match kind with
         | BiFinite -> 0
-        | Finite | CoFinite -> inference_nonuniform_params_off (); 0 in
+        | Finite | CoFinite ->
+          if (allparams <> []) then inference_nonuniform_params_off ();
+          0 in
   let allparams = EConstr.of_rel_context allparams in
   let allparams = safe_combine2_impls allparams i_impls ~default2:Glob_term.Explicit |> param2ctx in
   let nuparams, params = CList.chop nuparamsno allparams in
@@ -2663,10 +3235,11 @@ let inductive_entry2lp ~depth coq_ctx constraints state e =
     (* FIXME, arity could be longer *)
     { id; arity = nuparams; typ = EConstr.of_constr typ }) constructors in
   let ind = { params; decl = Inductive { id; nuparams; typ; kind; constructors } } in
-  hoas_ind2lp ~depth coq_ctx state ind
+  let state, i, gls = hoas_ind2lp ~depth coq_ctx state ind in
+  state, upoly_decl_of i, gls @ upoly_decl_gls
 ;;
 
-let record_entry2lp ~depth coq_ctx constraints state e =
+let record_entry2lp ~depth coq_ctx constraints state ~loose_udecl e =
   let open Record.Record_decl in
   let open Record.Data in
   let open Entries in
@@ -2683,20 +3256,18 @@ let record_entry2lp ~depth coq_ctx constraints state e =
   | [ x ] -> x
   | _ -> nYI "mutual record" in
   let indno = 1 in
-  
-  if not (Names.Id.Map.is_empty ubinders) then nYI "universe binders record";
-  if not (Names.Id.Map.is_empty (snd globnames)) then nYI "universe gbinders record";
-  
+    
   let state = global_univ_decls |> Option.cata (fun ctx ->
       S.update engine state (fun e ->
         { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma ctx})) state in
 
   let state = match mie.mind_entry_universes with
-    | Template_ind_entry ctx ->
-      S.update engine state (fun e ->
-        { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma ctx})
+    | Template_ind_entry _ -> nYI "template polymorphic inductives"
     | Monomorphic_ind_entry -> state
-    | Polymorphic_ind_entry _ -> nYI "univpoly ind" in
+    | Polymorphic_ind_entry cs -> S.update engine state (fun e ->
+      { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma (Univ.ContextSet.of_context cs) }) (* ???? *) in
+  
+  let state, upoly_decl_of, upoly_decl_gls = upoly_decl_of ~depth state ~loose_udecl mie in
 
   let params = mie.mind_entry_params in
   let params = Vars.lift_rel_context indno params in
@@ -2725,7 +3296,11 @@ let record_entry2lp ~depth coq_ctx constraints state e =
     ) (List.rev record.coers) kctx in
 
   let ind = { params; decl = Record { id; kid; typ; fields } } in
-  hoas_ind2lp ~depth coq_ctx state ind
+  let state, i, gls = hoas_ind2lp ~depth coq_ctx state ind in
+  state, upoly_decl_of i, gls @ upoly_decl_gls
+
+let merge_universe_context state uctx =
+  S.update engine state (fun e -> { e with sigma = Evd.merge_universe_context e.sigma uctx })
 
 (* ********************************* }}} ********************************** *)
 (* ****************************** API ********************************** *)
diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli
index ec96ccb9d..8f56467e4 100644
--- a/src/coq_elpi_HOAS.mli
+++ b/src/coq_elpi_HOAS.mli
@@ -16,6 +16,20 @@ type hole_mapping =
   | Verbatim   (* 1:1 correspondence between UVar and Evar *)
   | Heuristic  (* new UVar outside Llam is pruned before being linked to Evar *)
   | Implicit   (* No link, UVar is intepreted as a "hole" constant *)
+type uinstanceoption =
+  | NoInstance
+    (* the elpi command involved has to generate a fresh instance *)
+  | ConcreteInstance of Univ.Instance.t
+    (* a concrete instance was provided, the command will use it *)
+  | VarInstance of (FlexibleData.Elpi.t * RawData.term list * inv_rel_key)
+    (* a variable was provided, the command will compute the instance to unify with it *)
+
+type universe_decl = (Univ.Level.t list * bool) * (Univ.Constraints.t * bool)
+type universe_decl_cumul = ((Univ.Level.t * Univ.Variance.t option) list  * bool) * (Univ.Constraints.t * bool)
+type universe_decl_option =
+  | NotUniversePolymorphic
+  | Cumulative of universe_decl_cumul
+  | NonCumulative of universe_decl
 type options = {
   hoas_holes : hole_mapping option;
   local : bool option;
@@ -27,6 +41,8 @@ type options = {
   pplevel : Constrexpr.entry_relative_level;
   using : string option;
   inline : Declaremods.inline;
+  uinstance : uinstanceoption;
+  universe_decl : universe_decl_option;
 }
 
 type 'a coq_context = {
@@ -90,18 +106,18 @@ type record_field_spec = { name : Name.t; is_coercion : bool; is_canonical : boo
 
 val lp2inductive_entry :
   depth:int -> empty coq_context -> constraints -> State.t -> term ->
-  State.t * (Entries.mutual_inductive_entry * Univ.ContextSet.t * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
+  State.t * (Entries.mutual_inductive_entry * Univ.ContextSet.t * UnivNames.universe_binders * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
 
 val inductive_decl2lp :
-  depth:int -> empty coq_context -> constraints -> State.t -> (Names.MutInd.t * (Declarations.mutual_inductive_body * Declarations.one_inductive_body) * (Glob_term.binding_kind list * Glob_term.binding_kind list list)) ->
+  depth:int -> empty coq_context -> constraints -> State.t -> (Names.MutInd.t * Univ.Instance.t * (Declarations.mutual_inductive_body * Declarations.one_inductive_body) * (Glob_term.binding_kind list * Glob_term.binding_kind list list)) ->
     State.t * term * Conversion.extra_goals
 
 val inductive_entry2lp :
-  depth:int -> empty coq_context -> constraints -> State.t -> ComInductive.Mind_decl.t ->
+  depth:int -> empty coq_context -> constraints -> State.t -> loose_udecl:bool -> ComInductive.Mind_decl.t ->
     State.t * term * Conversion.extra_goals
 
 val record_entry2lp :
-  depth:int -> empty coq_context -> constraints -> State.t -> Record.Record_decl.t ->
+  depth:int -> empty coq_context -> constraints -> State.t -> loose_udecl:bool ->Record.Record_decl.t ->
     State.t * term * Conversion.extra_goals
   
 val in_elpi_id : Names.Name.t -> term
@@ -123,8 +139,10 @@ val unspec2opt : 'a Elpi.Builtin.unspec -> 'a option
 val opt2unspec : 'a option -> 'a Elpi.Builtin.unspec
 
 val in_elpi_gr : depth:int -> State.t -> Names.GlobRef.t -> term
-val in_elpi_sort : Sorts.t -> term
+val in_elpi_poly_gr : depth:int -> State.t -> Names.GlobRef.t -> term -> term
+val in_elpi_poly_gr_instance : depth:int -> State.t -> Names.GlobRef.t -> Univ.Instance.t -> term
 val in_elpi_flex_sort : term -> term
+val in_elpi_sort : depth:int -> state -> Sorts.t -> state * term
 val in_elpi_prod : Name.t -> term -> term -> term
 val in_elpi_lam : Name.t -> term -> term -> term
 val in_elpi_let : Name.t -> term -> term -> term -> term
@@ -149,7 +167,7 @@ val gref : Names.GlobRef.t Conversion.t
 val inductive : inductive Conversion.t
 val constructor : constructor Conversion.t
 val constant : global_constant Conversion.t
-val universe : Sorts.t Conversion.t
+val sort : Sorts.t Conversion.t
 val global_constant_of_globref : Names.GlobRef.t -> global_constant
 val abbreviation : Globnames.abbreviation Conversion.t
 val implicit_kind : Glob_term.binding_kind Conversion.t
@@ -160,15 +178,35 @@ type primitive_value =
   | Projection of Projection.t
 val primitive_value : primitive_value Conversion.t
 val in_elpi_primitive : depth:int -> state -> primitive_value -> state * term
+val uinstance : Univ.Instance.t Conversion.t
+
+val universe_constraint : Univ.univ_constraint Conversion.t
+val universe_variance : (Univ.Level.t * Univ.Variance.t option) Conversion.t
+val universe_decl : universe_decl Conversion.t
+val universe_decl_cumul : universe_decl_cumul Conversion.t
 
 module GRMap : Elpi.API.Utils.Map.S with type key = Names.GlobRef.t
 module GRSet : Elpi.API.Utils.Set.S with type elt = Names.GlobRef.t
 
+module UnivMap : Elpi.API.Utils.Map.S with type key = Univ.Universe.t
+module UnivSet : Elpi.API.Utils.Set.S with type elt = Univ.Universe.t
+
+module UnivLevelMap : Elpi.API.Utils.Map.S with type key = Univ.Level.t
+module UnivLevelSet : Elpi.API.Utils.Set.S with type elt = Univ.Level.t
+
+
+val compute_with_uinstance :
+  depth:int -> options -> state ->
+  (state -> 'a -> Univ.Instance.t option -> state * 'c * Univ.Instance.t option) ->
+  'a ->
+  Univ.Instance.t option ->
+    state * 'c * Univ.Instance.t option * Conversion.extra_goals
+
 (* CData relevant for other modules, e.g the one exposing Coq's API *)
+val universe_level_variable : Univ.Level.t Conversion.t
+val univ : Univ.Universe.t Conversion.t
 val isuniv : RawOpaqueData.t -> bool
-val univout : RawOpaqueData.t -> Sorts.t
-val univin : Sorts.t -> term
-val univ : Sorts.t Conversion.t
+val univout : RawOpaqueData.t -> Univ.Universe.t
 
 val is_sort : depth:int -> term -> bool
 val is_prod : depth:int -> term -> (term * term) option (* ty, bo @ depth+1 *)
@@ -195,10 +233,13 @@ type record_field_att =
   | Canonical of bool
 val record_field_att : record_field_att Conversion.t
 
-val new_univ : State.t -> State.t * Sorts.t
 val add_constraints : State.t -> UnivProblem.Set.t -> State.t
-val type_of_global : State.t -> Names.GlobRef.t -> State.t * EConstr.types
-val body_of_constant : State.t -> Names.Constant.t -> State.t * EConstr.t option
+val mk_global : State.t -> Names.GlobRef.t -> Univ.Instance.t option ->
+  State.t * EConstr.t * Univ.Instance.t option
+val poly_ctx_size_of_gref : Environ.env -> Names.GlobRef.t -> int
+val body_of_constant :
+  State.t -> Names.Constant.t -> Univ.Instance.t option ->
+  State.t * EConstr.t option * Univ.Instance.t option
 
 val command_mode : State.t -> bool
 val grab_global_env : State.t -> State.t
@@ -217,6 +258,7 @@ val pop_env : State.t -> State.t
 
 val get_global_env : State.t -> Environ.env
 val get_sigma : State.t -> Evd.evar_map
+val update_sigma : State.t -> (Evd.evar_map -> Evd.evar_map) -> State.t
 
 type hyp = { ctx_entry : term; depth : int }
 
@@ -229,3 +271,19 @@ val tclSOLUTION2EVD : Evd.evar_map -> 'a Elpi.API.Data.solution -> unit Proofvie
 
 val show_coq_engine : ?with_univs:bool -> State.t -> string
 val show_coq_elpi_engine_mapping : State.t -> string
+
+val type_of_global : state -> GlobRef.t -> Univ.Instance.t option -> state * (EConstr.t * Univ.Instance.t)
+val minimize_universes : state -> state
+val new_univ_level_variable : state -> state * (Univ.Level.t * Univ.Universe.t)
+val constraint_eq : Sorts.t -> Sorts.t -> UnivProblem.t
+val constraint_leq : Sorts.t -> Sorts.t -> UnivProblem.t
+val add_universe_constraint : state -> UnivProblem.t -> state
+val force_level_of_universe : state -> Univ.Universe.t -> state * Univ.Level.t * Univ.Universe.t * Sorts.t
+val ideclc : constant
+val uideclc : constant
+val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.universe_decl * Entries.variance_entry
+val merge_universe_context : state -> UState.t -> state
+val restricted_sigma_of : Univ.Level.Set.t -> state -> Evd.evar_map
+val universes_of_term : state -> EConstr.t -> Univ.Level.Set.t
+val universes_of_udecl : state -> UState.universe_decl -> Univ.Level.Set.t
+
diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml
index 67b2e5247..fd51c19df 100644
--- a/src/coq_elpi_arg_HOAS.ml
+++ b/src/coq_elpi_arg_HOAS.ml
@@ -55,20 +55,24 @@ type top_record_decl = Geninterp.interp_sign * glob_record_decl
 type raw_indt_decl = Vernacentries.Preprocessed_Mind_decl.inductive
 type glob_indt_decl = Genintern.glob_sign * raw_indt_decl
 type top_indt_decl = Geninterp.interp_sign * glob_indt_decl
-  
+
+type univpoly = Mono | Poly | CumulPoly
+
 type raw_record_decl_elpi = {
   name : qualified_name;
   parameters : Constrexpr.local_binder_expr list;
   sort : Constrexpr.sort_expr option;
   constructor : Names.Id.t option;
-  fields : (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr) list
+  fields : (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr) list;
+  univpoly : univpoly;
 } 
 type glob_record_decl_elpi = {
   name : string list * Names.Id.t;
   constructorname : Names.Id.t option;
   params : Glob_term.glob_decl list;
   arity : Glob_term.glob_constr;
-  fields : (Glob_term.glob_constr * Coq_elpi_HOAS.record_field_spec) list
+  fields : (Glob_term.glob_constr * Coq_elpi_HOAS.record_field_spec) list;
+  univpoly : univpoly;
 }
 
 let pr_raw_record_decl _ _ _ = Pp.str "TODO: pr_raw_record_decl"
@@ -82,6 +86,7 @@ type raw_indt_decl_elpi = {
   non_uniform_parameters : Constrexpr.local_binder_expr list option;
   arity : Constrexpr.constr_expr option;
   constructors : (Names.lident * Constrexpr.constr_expr) list;
+  univpoly : univpoly;
 }
 type glob_indt_decl_elpi = {
   finiteness : Declarations.recursivity_kind;
@@ -91,6 +96,7 @@ type glob_indt_decl_elpi = {
   nuparams : Glob_term.glob_decl list;
   nuparams_given : bool;
   constructors : (Names.Id.t * Glob_term.glob_constr) list;
+  univpoly : univpoly;
 }
 
 let pr_raw_indt_decl _ _ _ = Pp.str "TODO: pr_raw_indt_decl"
@@ -99,12 +105,15 @@ let pr_top_indt_decl _ _ _ = Pp.str "TODO: pr_top_indt_decl"
 
 type raw_constant_decl = {
   name : qualified_name;
+  atts : Attributes.vernac_flags;
+  udecl : Constrexpr.universe_decl_expr option;
   typ : Constrexpr.local_binder_expr list * Constrexpr.constr_expr option;
   body : Constrexpr.constr_expr option;
   red : Genredexpr.raw_red_expr option;
 }
 type glob_constant_decl_elpi = {
   name : string list * Names.Id.t;
+  udecl : universe_decl_option;
   params : Glob_term.glob_decl list;
   typ : Glob_term.glob_constr;
   body : Glob_term.glob_constr option;
@@ -181,6 +190,12 @@ let sep_last_qualid = function
   | [] -> "_", []
   | l -> CList.sep_last l
 
+let univpoly_of ~poly ~cumulative =
+  match poly, cumulative with
+  | true, true -> CumulPoly
+  | true, false -> Poly
+  | false, _ -> Mono
+
   let of_coq_inductive_definition id =
     let open Vernacentries.Preprocessed_Mind_decl in
     let { flags; typing_flags; private_ind; uniform; inductives } = id in
@@ -193,13 +208,17 @@ let sep_last_qualid = function
           List.map (fun (coercion,c) ->
             if coercion then CErrors.user_err Pp.(str "coercion flag not supported");
             c) constructors in
+    let { template; udecl; cumulative; poly; finite } = flags in
+    if template <> None then nYI "raw template polymorphic inductives";
+    if udecl <> None then nYI "raw universe polymorphic inductives with universe declaration";
     {
-      finiteness = flags.finite;
+      finiteness = finite;
       name;
       parameters;
       non_uniform_parameters;
       arity;
       constructors;
+      univpoly = univpoly_of ~poly ~cumulative
     }
   let of_coq_record_definition id =
     let open Vernacentries.Preprocessed_Mind_decl in
@@ -213,17 +232,21 @@ let sep_last_qualid = function
       match sort.CAst.v with
       | Constrexpr.CSort s -> s
       | _ -> CErrors.user_err ?loc:sort.CAst.loc Pp.(str "only explicits sorts are supported")) in
+    let { template; udecl; cumulative; poly; finite } = flags in
+    if template <> None then nYI "raw template polymorphic inductives";
+    if udecl <> None then nYI "raw universe polymorphic inductives with universe declaration";
     {
       name;
       parameters = binders;
       sort;
       constructor = Some idbuild;
-      fields = cfs
+      fields = cfs;
+      univpoly = univpoly_of ~poly ~cumulative
     } 
 
 let intern_record_decl glob_sign (it : raw_record_decl) = glob_sign, it
 
-let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fields } : raw_record_decl_elpi) : glob_record_decl_elpi =
+let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fields; univpoly } : raw_record_decl_elpi) : glob_record_decl_elpi =
   let name, space = sep_last_qualid name in
   let sort = match sort with
     | Some x -> Constrexpr.CSort x
@@ -247,9 +270,9 @@ let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fi
         gs, intern_env, (x, atts) :: acc
     | Vernacexpr.DefExpr _, _ -> Coq_elpi_utils.nYI "DefExpr")
         (glob_sign_params,intern_env,[]) fields in
-  { name = (space, Names.Id.of_string name); arity; params; constructorname = constructor; fields = List.rev fields }
+  { name = (space, Names.Id.of_string name); arity; params; constructorname = constructor; fields = List.rev fields; univpoly }
 
-let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform_parameters; arity; constructors } : raw_indt_decl_elpi) : glob_indt_decl_elpi =
+let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform_parameters; arity; constructors; univpoly } : raw_indt_decl_elpi) : glob_indt_decl_elpi =
   let name, space = sep_last_qualid name in
   let name = Names.Id.of_string name in
   let indexes = match arity with
@@ -274,7 +297,7 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform
   let constructors =
     List.map (fun (id,ty) -> id.CAst.v,
       intern_global_constr_ty glob_sign_params_self ~intern_env ty) constructors in
-  { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors }
+  { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly }
 let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it
 
 let expr_hole = CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None)
@@ -288,8 +311,23 @@ let raw_decl_name_to_glob name =
   let name, space = sep_last_qualid name in
   (space, Names.Id.of_string name)
 
-let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); body; red } =
+let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); body; red; udecl; atts } =
   let env = coq_ctx.env in
+  let poly =
+    let open Attributes in
+    parse polymorphic atts in
+  let state, udecl =
+    match udecl, poly with
+    | _, false -> state, NotUniversePolymorphic
+    | None, true -> state, NonCumulative (([],true),(Univ.Constraints.empty,true))
+    | Some udecl, true ->
+        let open UState in
+        let sigma,  { univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints; univdecl_instance} =
+          Constrintern.interp_univ_decl_opt (Coq_elpi_HOAS.get_global_env state) (Some udecl) in
+        let ustate = Evd.evar_universe_context sigma in
+        let u2n x = UState.universe_of_name ustate x.CAst.v in
+        let state = merge_universe_context state ustate in
+        state, NonCumulative ((List.map u2n univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in
   let sigma = get_sigma state in
   match body, typ with
   | Some body, _ ->
@@ -300,25 +338,40 @@ let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); bod
       in
       let state, gls0 = set_current_sigma ~depth state sigma in
       let typ = option_default (fun () -> Retyping.get_type_of env sigma body) typ in
-      state, typ, Some body, gls0 
+      state, udecl, typ, Some body, gls0 
   | None, Some typ ->
       assert(red = None);
       let sigma, typ, impargs =
         ComAssumption.interp_assumption ~program_mode:false
           env sigma Constrintern.empty_internalization_env bl typ in
       let state, gls0 = set_current_sigma ~depth state sigma in
-      state, typ, None, gls0
+      state, udecl, typ, None, gls0
   | _ -> assert false
 
 
-let raw_constant_decl_to_glob glob_sign ({ name; typ = (params,typ); body } : raw_constant_decl) =
+let raw_constant_decl_to_glob glob_sign ({ name; atts; udecl; typ = (params,typ); body } : raw_constant_decl) state =
   let intern_env, params = intern_global_context glob_sign ~intern_env:Constrintern.empty_internalization_env params in
   let glob_sign_params = push_glob_ctx params glob_sign in
   let params = List.rev params in
   let typ = Option.default expr_hole typ in
   let typ = intern_global_constr_ty ~intern_env glob_sign_params typ in
   let body = Option.map (intern_global_constr ~intern_env glob_sign_params) body in
-  { name = raw_decl_name_to_glob name; params; typ; body }
+  let poly =
+    let open Attributes in
+    parse polymorphic atts in
+  let state, udecl =
+    match udecl, poly with
+    | _, false -> state, NotUniversePolymorphic
+    | None, true -> state, NonCumulative (([],true),(Univ.Constraints.empty,true))
+    | Some udecl, true ->
+        let open UState in
+        let sigma,  { univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints; univdecl_instance} =
+          Constrintern.interp_univ_decl_opt (Coq_elpi_HOAS.get_global_env state) (Some udecl) in
+        let ustate = Evd.evar_universe_context sigma in
+        let u2n x = UState.universe_of_name ustate x.CAst.v in
+        let state = merge_universe_context state ustate in
+        state, NonCumulative ((List.map u2n univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in
+  state, { name = raw_decl_name_to_glob name; params; typ; udecl; body }
 let intern_constant_decl glob_sign (it : raw_constant_decl) = glob_sign, it
 
 let glob glob_sign : raw -> glob = function
@@ -446,13 +499,23 @@ let wit = add_genarg "elpi_ftactic_arg"
 
 end
 
-
-
-let grecord2lp ~depth state { Cmd.name; arity; params; constructorname; fields } =
+let mk_indt_decl state univpoly r =
+  match univpoly with
+  | Cmd.Mono -> state, E.mkApp ideclc r []
+  | Cmd.Poly -> 
+      let state, up, gls = universe_decl.API.Conversion.embed ~depth:0 state (([],true),(Univ.Constraints.empty,true)) in
+      assert(gls=[]);
+      state, E.mkApp uideclc r [up]
+  | Cmd.CumulPoly ->
+      let state, up, gls = universe_decl_cumul.API.Conversion.embed ~depth:0 state (([],true),(Univ.Constraints.empty,true)) in
+      assert(gls=[]);
+      state, E.mkApp uideclc r [up]
+
+let grecord2lp ~depth state { Cmd.name; arity; params; constructorname; fields; univpoly } =
   let open Coq_elpi_glob_quotation in
   let state, r = do_params params (do_record ~name ~constructorname arity fields) ~depth state in
-  state, r
-
+  mk_indt_decl state univpoly r
+  
 let contract_params env sigma name params nuparams_given t =
   if nuparams_given then t else
   let open Glob_term in
@@ -494,7 +557,7 @@ let drop_unit f ~depth state =
   state, x
   
 
-let ginductive2lp ~depth state { Cmd.finiteness; name; arity; params; nuparams; nuparams_given; constructors } =
+let ginductive2lp ~depth state { Cmd.finiteness; name; arity; params; nuparams; nuparams_given; constructors; univpoly } =
   let open Coq_elpi_glob_quotation in
   let space, indt_name = name in
   let contract state x = contract_params (get_global_env state) (get_sigma state) indt_name params nuparams_given x in
@@ -513,7 +576,7 @@ let ginductive2lp ~depth state { Cmd.finiteness; name; arity; params; nuparams;
     ~depth state
   in
   let state, r = do_params params (drop_unit do_inductive) ~depth state in
-  state, r
+  mk_indt_decl state univpoly r
 
 let in_option = Elpi.(Builtin.option API.BuiltInData.any).API.Conversion.embed
 
@@ -523,11 +586,21 @@ let decl_name2lp name =
     Id.of_string_soft @@ String.concat "." (space @ [Id.to_string constant_name]) in
   in_elpi_id (Name.Name qconstant_name)
 
-let cdecl2lp ~depth state { Cmd.name; params; typ; body } =
+let cdeclc = E.Constants.declare_global_symbol "const-decl"
+let ucdeclc = E.Constants.declare_global_symbol "upoly-const-decl"
+
+let cdecl2lp ~depth state { Cmd.name; params; typ; body; udecl } =
   let open Coq_elpi_glob_quotation in
   let state, typ = do_params params (do_arity typ) ~depth state in
   let state, body = option_map_acc (fun state bo -> gterm2lp ~depth state @@ Coq_elpi_utils.mk_gfun bo params) state body in
-  state, decl_name2lp name, typ, body
+  let name = decl_name2lp name in
+  let state, body, gls = in_option ~depth state body in
+  match udecl with
+  | NotUniversePolymorphic -> state, E.mkApp cdeclc name [body;typ], gls
+  | Cumulative _ -> assert false
+  | NonCumulative ud ->
+      let state, ud, gls1 = universe_decl.API.Conversion.embed ~depth state ud in
+      state, E.mkApp ucdeclc name [body;typ;ud], gls @ gls1
 
 let ctxitemc = E.Constants.declare_global_symbol "context-item"
 let ctxendc =  E.Constants.declare_global_symbol "context-end"
@@ -564,8 +637,6 @@ let rec do_context_constr coq_ctx csts fields ~depth state =
 let strc = E.Constants.declare_global_symbol "str"
 let trmc = E.Constants.declare_global_symbol "trm"
 let intc = E.Constants.declare_global_symbol "int"
-let ideclc = E.Constants.declare_global_symbol "indt-decl"
-let cdeclc = E.Constants.declare_global_symbol "const-decl"
 let ctxc = E.Constants.declare_global_symbol "ctx-decl"
 
 let my_cast_to_string v =
@@ -673,6 +744,11 @@ let in_elpi_tac ~depth ?calldepth coq_ctx hyps sigma state x =
   | String x -> singleton @@ in_elpi_string_arg ~depth state x
   | Term (ist,glob_or_expr) -> singleton @@ in_elpi_term_arg ~depth state coq_ctx hyps sigma ist glob_or_expr
 
+let handle_template_polymorphism = function
+  | None -> Some false
+  | Some false -> Some false
+  | Some true -> err Pp.(str "#[universes(template)] is not supported")
+
 let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
   let open Cmd in
   let hyps = [] in
@@ -682,25 +758,24 @@ let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
       let glob_rdecl = raw_record_decl_to_glob glob_sign raw_rdecl in
       let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
       let state, t = grecord2lp ~depth state glob_rdecl in
-      state, E.mkApp ideclc t [], []
+      state, t, []
   | RecordDecl (_ist,(glob_sign,raw_rdecl)) ->
-      let e =
-        let open Vernacentries.Preprocessed_Mind_decl in
-        let { flags = { template; poly; cumulative; udecl; finite }; primitive_proj; kind; records } = raw_rdecl in
-        Record.interp_structure ~template udecl kind ~cumulative ~poly ~primitive_proj finite records
-      in
-      let state, t, gls = record_entry2lp ~depth coq_ctx E.no_constraints state e in
-      state, E.mkApp ideclc t [], gls
+      let open Vernacentries.Preprocessed_Mind_decl in
+      let { flags = { template; poly; cumulative; udecl; finite }; primitive_proj; kind; records } = raw_rdecl in
+      let template = handle_template_polymorphism template in
+      let e = Record.interp_structure ~template udecl kind ~cumulative ~poly ~primitive_proj finite records in
+      record_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e
   | IndtDecl (_ist,(glob_sign,raw_indt)) when raw ->
       let raw_indt = of_coq_inductive_definition raw_indt in
       let glob_indt = raw_indt_decl_to_glob glob_sign raw_indt in
       let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
       let state, t = ginductive2lp ~depth state glob_indt in
-      state, E.mkApp ideclc t [], []
+      state, t, []
   | IndtDecl (_ist,(glob_sign,raw_indt)) -> 
+      let open Vernacentries.Preprocessed_Mind_decl in
+      let { flags = { template; poly; cumulative; udecl; finite }; typing_flags; uniform; private_ind; inductives } = raw_indt in
+      let template = handle_template_polymorphism template in
       let e =
-        let open Vernacentries.Preprocessed_Mind_decl in
-        let { flags = { template; poly; cumulative; udecl; finite }; typing_flags; uniform; private_ind; inductives } = raw_indt in
         match inductives with
         | [mind_w_not] ->
             ComInductive.interp_mutual_inductive ~env:coq_ctx.env
@@ -708,16 +783,13 @@ let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
               udecl [mind_w_not] finite
         | _ -> nYI "(HOAS) mutual inductives"
       in
-      let state, t, gls = inductive_entry2lp ~depth coq_ctx E.no_constraints state e in
-      state, E.mkApp ideclc t [], gls
+      inductive_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e
   | ConstantDecl (_ist,(glob_sign,raw_cdecl)) when raw ->
-      let glob_cdecl = raw_constant_decl_to_glob glob_sign raw_cdecl in
+      let state, glob_cdecl = raw_constant_decl_to_glob glob_sign raw_cdecl state in
       let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
-      let state, c, typ, body = cdecl2lp ~depth state glob_cdecl in
-      let state, body, gls = in_option ~depth state body in
-      state, E.mkApp cdeclc c [body;typ], gls
+      cdecl2lp ~depth state glob_cdecl
   | ConstantDecl (_ist,(glob_sign,({ name; typ = (bl,_) } as raw_cdecl))) ->
-      let state, typ, body, gls0 =
+      let state, udecl, typ, body, gls0 =
         raw_constant_decl_to_constr ~depth coq_ctx state raw_cdecl in
       let state, typ, gls1 = constr2lp_closed ~depth ?calldepth coq_ctx E.no_constraints state typ in
       let state, body, gls2 =
@@ -725,7 +797,13 @@ let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
       let state, typ = best_effort_recover_arity ~depth state typ bl in
       let state, body, _ = in_option ~depth state body in
       let c = decl_name2lp (raw_decl_name_to_glob name) in
-      state, E.mkApp cdeclc c [body;typ], gls0 @ gls1 @ gls2
+      begin match udecl with
+      | NotUniversePolymorphic -> state, E.mkApp cdeclc c [body;typ], gls0 @ gls1 @ gls2
+      | Cumulative _ -> assert false
+      | NonCumulative udecl ->
+          let state, ud, gls3 = universe_decl.API.Conversion.embed ~depth state udecl in
+          state, E.mkApp ucdeclc c [body;typ;ud], gls0 @ gls1 @ gls2 @ gls3
+      end
   | Context (_ist,(glob_sign,raw_ctx)) when raw ->
       let glob_ctx = raw_context_decl_to_glob glob_sign raw_ctx in
       let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in
diff --git a/src/coq_elpi_arg_HOAS.mli b/src/coq_elpi_arg_HOAS.mli
index fe1dec2e2..56d3901b8 100644
--- a/src/coq_elpi_arg_HOAS.mli
+++ b/src/coq_elpi_arg_HOAS.mli
@@ -21,6 +21,8 @@ type top_indt_decl = Geninterp.interp_sign * glob_indt_decl
 
 type raw_constant_decl = {
   name : qualified_name;
+  atts : Attributes.vernac_flags;
+  udecl : Constrexpr.universe_decl_expr option;
   typ : Constrexpr.local_binder_expr list * Constrexpr.constr_expr option;
   body : Constrexpr.constr_expr option;
   red : Genredexpr.raw_red_expr option;
diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg
index ccd510daf..4320f4e1d 100644
--- a/src/coq_elpi_arg_syntax.mlg
+++ b/src/coq_elpi_arg_syntax.mlg
@@ -161,6 +161,12 @@ let of_coq_record_declaration ~atts kind id =
   | Inductive _ -> assert false
   | Record r -> r
 
+let of_coq_definition ~loc ~atts name udecl def =
+  match def with
+  | Vernacexpr.DefineBody(bl,red,c,ty) ->
+      EA.Cmd.(ConstantDecl { name = snd name; atts; udecl; typ = (bl,ty); red; body = Some c })
+  | Vernacexpr.ProveBody _ ->
+      CErrors.user_err ~loc Pp.(str"syntax error: missing Definition body")
 
 }
 
@@ -235,15 +241,13 @@ GLOB_PRINTED BY { fun _ _ _ -> EA.Cmd.pp_glob env sigma }
 | [ "Structure" inductive_or_record_definition(id) ] -> { EA.Cmd.RecordDecl (of_coq_record_declaration ~atts:[] Vernacexpr.Structure id) }  
 | [ "#[" attributes(atts) "]" "Structure" inductive_or_record_definition(id) ] -> { EA.Cmd.RecordDecl (of_coq_record_declaration ~atts Vernacexpr.Structure id) }  
 
-(* TODO attributes *)
-| [ "Definition" qualified_name(name) def_body(def) ] -> {
-      match def with
-      | Vernacexpr.DefineBody(bl,red,c,ty) ->
-          EA.Cmd.(ConstantDecl { name = snd name; typ = (bl,ty); red; body = Some c })
-      | Vernacexpr.ProveBody _ ->
-          CErrors.user_err ~loc Pp.(str"syntax error: missing Definition body") }
-| [ "Axiom" qualified_name(name) telescope(typ) colon_constr(t) ] -> {
-      EA.Cmd.(ConstantDecl { name = snd name; typ = (typ,Some t); red = None; body = None }) }
+| [ "Definition" qualified_name(name) univ_decl_opt(udecl) def_body(def) ] -> { of_coq_definition ~loc ~atts:[] name udecl def }
+| [ "#[" attributes(atts) "]" "Definition" qualified_name(name) univ_decl_opt(udecl) def_body(def) ] -> { of_coq_definition ~loc ~atts name udecl def }
+
+| [ "Axiom" qualified_name(name) univ_decl_opt(udecl) telescope(typ) colon_constr(t) ] -> {
+      EA.Cmd.(ConstantDecl { name = snd name; atts = []; udecl; typ = (typ,Some t); red = None; body = None }) }
+| [ "#[" attributes(atts) "]" "Axiom" qualified_name(name) univ_decl_opt(udecl) telescope(typ) colon_constr(t) ] -> {
+      EA.Cmd.(ConstantDecl { name = snd name; atts; udecl; typ = (typ,Some t); red = None; body = None }) }
 
 
 | [ "Context" telescope(ty) ] -> { EA.Cmd.Context ty }
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 7159b38e6..47b8ec906 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -12,10 +12,14 @@ module B = struct
   include API.BuiltInData
   include Elpi.Builtin
   let ioarg = API.BuiltInPredicate.ioarg
+  let ioarg_any = API.BuiltInPredicate.ioarg_any
   let ioargC = API.BuiltInPredicate.ioargC
   let ioargC_flex = API.BuiltInPredicate.ioargC_flex
+  let ioarg_flex = API.BuiltInPredicate.ioarg_flex
+  let ioarg_poly s = { ioarg_any with API.Conversion.ty = API.Conversion.TyName s }
 end
 module Pred = API.BuiltInPredicate
+module U = API.Utils
 
 module CNotation = Notation
 
@@ -24,7 +28,6 @@ open Names
 open Coq_elpi_utils
 open Coq_elpi_HOAS
 
-
 let string_of_ppcmds options pp =
   let b = Buffer.create 512 in
   let fmt = Format.formatter_of_buffer b in
@@ -113,9 +116,7 @@ let on_global_state_does_rewind_env api thunk = (); (fun state ->
 
 let warn_if_contains_univ_levels ~depth t =
   let global_univs = UGraph.domain (Environ.universes (Global.env ())) in
-  let is_global u = match u with
-  | Sorts.Set | Sorts.SProp | Sorts.Prop -> true
-  | Sorts.Type u ->
+  let is_global u = 
     match Univ.Universe.level u with
     | None -> true
     | Some l -> Univ.Level.Set.mem l global_univs in
@@ -127,7 +128,7 @@ let warn_if_contains_univ_levels ~depth t =
   let univs = aux ~depth [] t in
   if univs <> [] then
     err Pp.(strbrk "The hypothetical clause contains terms of type univ which are not global, you should abstract them out or replace them by global ones: " ++
-            prlist_with_sep spc Sorts.debug_print univs)
+            prlist_with_sep spc Univ.Universe.pr univs)
 ;;
 
 let bool = B.bool
@@ -136,57 +137,9 @@ let list = B.list
 let pair = B.pair
 let option = B.option
 
-let constraint_leq u1 u2 =
-  let open UnivProblem in
-  ULe (u1, u2)
-
-let constraint_eq u1 u2 =
-  let open UnivProblem in
-  ULe (u1, u2)
-
-let add_universe_constraint state c =
-  let open UnivProblem in
-  try add_constraints state (Set.singleton c)
-  with
-  | UGraph.UniverseInconsistency p ->
-      Feedback.msg_debug
-        (UGraph.explain_universe_inconsistency
-           UnivNames.(pr_with_global_universes empty_binders) p);
-      raise Pred.No_clause
-  | Evd.UniversesDiffer | UState.UniversesDiffer ->
-      Feedback.msg_debug Pp.(str"UniversesDiffer");
-      raise Pred.No_clause
-
-let mk_fresh_univ state = new_univ state
-
 let mk_algebraic_super x = Sorts.super x
 
 (* I don't want the user to even know that algebraic universes exist *)
-let purge_1_algebraic_universe state s = match s with
-| Sorts.Set | Sorts.Prop | Sorts.SProp -> state, s
-| Sorts.Type u ->
-  if Univ.Universe.is_level u then state, s
-  else
-    let state, v = mk_fresh_univ state in
-    add_universe_constraint state (constraint_leq s v), v
-
-let purge_algebraic_univs state t =
-  let sigma = get_sigma state in
-  (* no map_fold iterator :-/ *)
-  let state = ref state in
-  let rec aux t =
-    match EConstr.kind sigma t with
-    | Constr.Sort s -> begin
-        match EConstr.ESorts.kind sigma s with
-        | Sorts.Type _ as u ->
-            let new_state, v = purge_1_algebraic_universe !state u in
-            state := new_state;
-            EConstr.mkSort v
-        | _ -> EConstr.map sigma aux t
-        end
-    | _ -> EConstr.map sigma aux t in
-  let t = aux t in
-  !state, t
 
 let univ_super state u v =
   let state, u = match u with
@@ -194,27 +147,25 @@ let univ_super state u v =
   | Sorts.Type ul ->
     if Univ.Universe.is_level ul then state, u
     else
-      let state, w = mk_fresh_univ state in
+      let state, (_,w) = new_univ_level_variable state in
+      let w = Sorts.sort_of_univ w in
       add_universe_constraint state (constraint_leq u w), w in
     add_universe_constraint state (constraint_leq (mk_algebraic_super u) v)
 
 let univ_product state s1 s2 =
   let s = Typeops.sort_of_product (get_global_env state) s1 s2 in
-  let state, v = mk_fresh_univ state in
-  let state =
-    add_universe_constraint state (constraint_leq s v) in
+  let state, (_,v) = new_univ_level_variable state in
+  let v = Sorts.sort_of_univ v in
+  let state = add_universe_constraint state (constraint_leq s v) in
   state, v
 
 let constr2lp ~depth hyps constraints state t =
-  let state, t = purge_algebraic_univs state t in
   constr2lp ~depth hyps constraints state t
 
 let constr2lp_closed ~depth hyps constraints state t =
-  let state, t = purge_algebraic_univs state t in
   constr2lp_closed ~depth hyps constraints state t
 
 let constr2lp_closed_ground ~depth hyps constraints state t =
-  let state, t = purge_algebraic_univs state t in
   constr2lp_closed_ground ~depth hyps constraints state t
 
 let clauses_for_later =
@@ -228,16 +179,18 @@ let clauses_for_later =
             Elpi.API.Pp.Ast.program code Coq_elpi_utils.pp_scope scope) l)
 ;;
 
+(*
 let univ = { univ with
   Conv.readback = (fun ~depth state x ->
     let state, u, gl = univ.Conv.readback ~depth state x in
-    let state, u = purge_1_algebraic_universe state u in
+    let state, _, u, _ = force_level_of_universe state u in
     state, u, gl);
   embed = (fun ~depth state x ->
-    let state, x = purge_1_algebraic_universe state x in
+    let state, _, x, _ = force_level_of_universe state x in
     let state, u, gl = univ.Conv.embed ~depth state x in
     state, u, gl);
 }
+*)
 
 let term = {
   CConv.ty = Conv.TyName "term";
@@ -306,7 +259,7 @@ let goal : ( (Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context * Evar.t * Coq_elpi_a
   embed = (fun ~depth _ _ _ _ -> assert false);
   readback = (fun ~depth hyps csts state g ->
     let state, ctx, k, raw_args, gls1 = Coq_elpi_HOAS.lp2goal ~depth hyps csts state g in
-    let state, args, gls2 = API.Utils.map_acc (Coq_elpi_arg_HOAS.in_coq_arg ~depth ctx csts) state raw_args in
+    let state, args, gls2 = U.map_acc (Coq_elpi_arg_HOAS.in_coq_arg ~depth ctx csts) state raw_args in
     state, (ctx,k,args), gls1 @ gls2);
 }
 
@@ -356,6 +309,22 @@ let is_mutual_inductive_entry_ground { Entries.mind_entry_params; mind_entry_ind
   List.for_all (is_ground_rel_ctx_entry sigma) mind_entry_params &&
   List.for_all (is_ground_one_inductive_entry sigma) mind_entry_inds
 
+let handle_uinst_option_for_inductive ~depth options i state =
+  match options.uinstance with
+  | NoInstance ->
+      let term, ctx = UnivGen.fresh_global_instance (get_global_env state) (GlobRef.IndRef i) in
+      let state = update_sigma state (fun sigma -> Evd.merge_context_set UState.univ_flexible_alg sigma ctx) in
+      snd @@ Constr.destInd term, state, []
+  | ConcreteInstance i -> i, state, []
+  | VarInstance (v_head, v_args, v_depth) ->
+      let v' = U.move ~from:v_depth ~to_:depth (E.mkUnifVar v_head ~args:v_args state) in
+      let term, ctx =
+        UnivGen.fresh_global_instance (get_global_env state) (GlobRef.IndRef i) in
+      let uinst = snd @@ Constr.destInd term in
+      let state, lp_uinst, extra_goals = uinstance.Conv.embed ~depth state uinst in
+      let state = update_sigma state (fun sigma -> Evd.merge_context_set UState.univ_flexible_alg sigma ctx) in
+      uinst, state, API.Conversion.Unify (v', lp_uinst) :: extra_goals
+
 type located =
   | LocGref of Names.GlobRef.t
   | LocModule of Names.ModPath.t
@@ -435,13 +404,14 @@ let cs_pattern =
     K("cs-default","",N,
       B Default_cs,
       M (fun ~ok ~ko -> function Default_cs -> ok | _ -> ko ()));
-    K("cs-sort","",A(universe,N),
+    K("cs-sort","",A(sort,N),
       B (fun s -> Sort_cs (Sorts.family s)),
       MS (fun ~ok ~ko p state -> match p with
         | Sort_cs Sorts.InSet -> ok Sorts.set state
         | Sort_cs Sorts.InProp -> ok Sorts.prop state
         | Sort_cs Sorts.InType ->
-              let state, u = mk_fresh_univ state in
+              let state, (_,u) = new_univ_level_variable state in
+              let u = Sorts.sort_of_univ u in
               ok u state
         | _ -> ko state))
   ]
@@ -675,35 +645,20 @@ let attribute = attribute attribute_value
 
 let warning = CWarnings.create ~name:"lib" ~category:"elpi" Pp.str
 
+let keep x = (x = Pred.Keep)
+
 let if_keep x f =
   match x with
   | Pred.Discard -> None
   | Pred.Keep -> Some (f ())
 
-let if_keep_acc x state f =
+let _if_keep_acc x state f =
   match x with
   | Pred.Discard -> state, None
   | Pred.Keep ->
        let state, x = f state in
        state, Some x
 
-let version_parser version =
-  let (!!) x = try int_of_string x with Failure _ -> -100 in
-  match Str.split (Str.regexp_string ".") version with
-  | major :: minor :: patch :: _ -> !!major, !!minor, !!patch
-  | [ major ] -> !!major,0,0
-  | [] -> 0,0,0
-  | [ major; minor ] ->
-      match Str.split (Str.regexp_string "+") minor with
-      | [ minor ] -> !!major, !!minor, 0
-      | [ ] -> !!major, !!minor, 0
-      | minor :: prerelease :: _ ->
-          if Str.string_match (Str.regexp_string "beta") prerelease 0 then
-            !!major, !!minor, !!("-"^String.sub prerelease 4 (String.length prerelease - 4))
-          else if Str.string_match (Str.regexp_string "alpha") prerelease 0 then
-            !!major, !!minor, !!("-"^String.sub prerelease 5 (String.length prerelease - 5))
-          else !!major, !!minor, -100
-
 let mp2path x =
   let rec mp2sl = function
     | MPfile dp -> CList.rev_map Id.to_string (DirPath.repr dp)
@@ -830,10 +785,15 @@ let warn_deprecated_add_axiom =
            "section variables is deprecated. Use coq.env.add-axiom or " ^
            "coq.env.add-section-variable instead"))
 
-let add_axiom_or_variable api id sigma ty local inline =
-  let used = EConstr.universes_of_constr sigma ty in
-  let sigma = Evd.restrict_universe_context sigma used in
-  let uentry = Evd.univ_entry ~poly:false sigma in
+let add_axiom_or_variable api id ty local options state =
+  let state, poly, cumul, udecl, _ = poly_cumul_udecl_variance_of_options state options in
+  let used = universes_of_term state ty in
+  let sigma = restricted_sigma_of used state in
+  if cumul then
+    err Pp.(str api ++ str": unsupported attribute @udecl-cumul! or @univpoly-cumul!");
+  if poly && local then
+    err Pp.(str api ++ str": section variables cannot be universe polymorphic");
+  let uentry = UState.check_univ_decl (Evd.evar_universe_context sigma) udecl ~poly in
   let kind = Decls.Logical in
   let impargs = [] in
   let variable = CAst.(make @@ Id.of_string id) in
@@ -844,8 +804,8 @@ let add_axiom_or_variable api id sigma ty local inline =
       ComAssumption.declare_variable false ~kind (EConstr.to_constr sigma ty) uentry impargs Glob_term.Explicit variable;
       GlobRef.VarRef(Id.of_string id), Univ.Instance.empty
     end else
-      ComAssumption.declare_axiom false ~local:Locality.ImportDefaultBehavior ~poly:false ~kind (EConstr.to_constr sigma ty)
-        uentry impargs inline
+      ComAssumption.declare_axiom false ~local:Locality.ImportDefaultBehavior ~poly ~kind (EConstr.to_constr sigma ty)
+        uentry impargs options.inline
         variable
   in
   gr
@@ -1050,6 +1010,58 @@ let hint_locality_doc = {|
 (*****************************************************************************)
 
 
+let unify_instances_gref gr ui1 ui2 diag env state cmp_constr_universes =
+  let open Pred in
+  let open Notation in
+  let nargs, poly_ctx_size =
+    let open Names.GlobRef in
+    match gr with
+    | VarRef _ -> 0, 0
+    | ConstRef c ->
+      let cb = Environ.lookup_constant c env in
+      let univs = Declareops.constant_polymorphic_context cb in
+      0, Univ.AbstractContext.size univs
+    | IndRef ind ->
+      let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+      let univs = Declareops.inductive_polymorphic_context mib in
+      Reduction.inductive_cumulativity_arguments (mib,snd ind), Univ.AbstractContext.size univs
+    | ConstructRef (ind,kno) ->
+      let (mib,_ as specif) =
+        Inductive.lookup_mind_specif env ind in
+      let univs = Declareops.inductive_polymorphic_context mib in
+      Reduction.constructor_cumulativity_arguments (mib,snd ind,kno), Univ.AbstractContext.size univs
+  in
+  let l1 = Univ.Instance.length ui1 in
+  let l2 = Univ.Instance.length ui2 in
+  if l1 <> l2 then
+    state, !: (B.mkERROR "different universe instance lengths"), []
+  else if l1 <> poly_ctx_size then
+    let msg =
+      Printf.sprintf "global reference %s expects instances of length %d, got %d"
+        (Pp.string_of_ppcmds (Printer.pr_global gr)) poly_ctx_size l1 in
+    state, !: (B.mkERROR msg), []
+  else
+    let t1 = EConstr.mkRef (gr, EConstr.EInstance.make ui1) in
+    let t2 = EConstr.mkRef (gr, EConstr.EInstance.make ui2) in
+    let sigma = get_sigma state in
+    match cmp_constr_universes env sigma ?nargs:(Some nargs) t1 t2 with
+    | None -> assert false
+    | Some problem_set ->
+      try
+        let state = add_constraints state problem_set in
+        state, !: B.mkOK, []
+      with
+      | Evd.UniversesDiffer | UState.UniversesDiffer ->
+        state, !: (B.mkERROR "UniversesDiffer"), []
+      | UGraph.UniverseInconsistency p ->
+        match diag with
+        | Data B.OK -> raise No_clause
+        | _ ->
+          let msg =
+            UGraph.explain_universe_inconsistency
+              UnivNames.(pr_with_global_universes empty_binders) p in
+          state, !: (B.mkERROR (Pp.string_of_ppcmds msg)), []
+
 let coq_builtins =
   let open API.BuiltIn in
   let open Pred in
@@ -1147,7 +1159,7 @@ line option|}))),
     Easy "Fetches the version of Coq, as a string and as 3 numbers")))),
     (fun _ _ _ _ ~depth:_ ->
       let version = Coq_config.version in
-      let major, minor, patch = version_parser version in
+      let major, minor, patch = coq_version_parser version in
       !: version +! major +! minor +! patch)),
   DocAbove);
   LPCode {|
@@ -1214,10 +1226,31 @@ It's a fatal error if Name cannot be located.|})),
   MLCode(Pred("coq.env.typeof",
     In(gref, "GR",
     COut(closed_ground_term, "Ty",
-    Full(global, "reads the type Ty of a global reference."))),
-  (fun gr _ ~depth _ _ state ->
-    let state, ty = type_of_global state gr in
-    state, !:ty, [])),
+    Full(global, {|reads the type Ty of a global reference.
+Supported attributes:
+- @uinstance! I (default: fresh instance I)|}))),
+  (fun gr _ ~depth { options } _ state ->
+    let type_of_global' state term inst_opt =
+      let state, (ty, inst) = type_of_global state term inst_opt in
+      state, ty, Some inst
+    in
+    let state, ty, _, gls =
+        compute_with_uinstance ~depth options state type_of_global' gr None in
+    state, !: ty, gls)),
+  DocAbove);
+
+  MLCode(Pred("coq.env.global",
+    In(gref, "GR",
+    COut(closed_ground_term, "T",
+    Full(global, {|turns a global reference GR into a term.
+T = (global GR) or, if GR points to a universe polymorphic term,
+T = (pglobal GR I).
+Supported attributes:
+- @uinstance! I (default: fresh instance I)|}))),
+  (fun gr _ ~depth { options } _ state ->
+    let state, t, _, gls =
+      compute_with_uinstance ~depth options state mk_global gr None in
+    state, !: t, gls)),
   DocAbove);
 
   MLCode(Pred("coq.env.indt",
@@ -1228,58 +1261,92 @@ It's a fatal error if Name cannot be located.|})),
     COut(closed_ground_term, "type of the inductive type constructor including parameters",
     Out(list constructor, "list of constructor names",
     COut(!>> B.list closed_ground_term, "list of the types of the constructors (type of KNames) including parameters",
-    Full(global, "reads the inductive type declaration for the environment")))))))),
-  (fun i _ _ _ arity knames ktypes ~depth { env } _ state ->
-     let open Declarations in
-     let mind, indbo as ind = lookup_inductive env i in
-     let co  = mind.mind_finite <> Declarations.CoFinite in
-     let lno = mind.mind_nparams in
-     let luno = mind.mind_nparams_rec in
-     let arity = if_keep arity (fun () ->
-       Inductive.type_of_inductive (ind,Univ.Instance.empty)
-       |> EConstr.of_constr) in
-     let knames = if_keep knames (fun () ->
-       CList.(init Declarations.(indbo.mind_nb_constant + indbo.mind_nb_args)
-           (fun k -> i,k+1))) in
-     let ktypes = if_keep ktypes (fun () ->
-       Inductive.type_of_constructors (i,Univ.Instance.empty) ind
-       |> CArray.map_to_list EConstr.of_constr) in
-     state, !: co +! lno +! luno +? arity +? knames +? ktypes, [])),
+    Full(global, {|reads the inductive type declaration for the environment.
+% Supported attributes:
+% - @uinstance! I (default: fresh instance I)|})))))))),
+  (fun i _ _ _ arity knames ktypes ~depth { env ; options } _ state ->
+    let open Declarations in
+    let mind, indbo as ind = lookup_inductive env i in
+    let co  = mind.mind_finite <> Declarations.CoFinite in
+    let lno = mind.mind_nparams in
+    let luno = mind.mind_nparams_rec in
+    let uinst, state, extra_goals = handle_uinst_option_for_inductive ~depth options i state in    
+    let arity = if_keep arity (fun () ->
+      Inductive.type_of_inductive (ind,uinst)
+      |> EConstr.of_constr) in
+    let knames = if_keep knames (fun () ->
+      CList.(init Declarations.(indbo.mind_nb_constant + indbo.mind_nb_args) (fun k -> i,k+1))) in
+    let ktypes = if_keep ktypes (fun () ->
+      Inductive.type_of_constructors (i,uinst) ind
+      |> CArray.map_to_list EConstr.of_constr) in
+    state, !: co +! lno +! luno +? arity +? knames +? ktypes, extra_goals)),
+
   DocNext);
 
   MLCode(Pred("coq.env.indt-decl",
     In(inductive, "reference to the inductive type",
     COut(indt_decl_out,"HOAS description of the inductive type",
-    Full(global,"reads the inductive type declaration for the environment"))),
-  (fun i _ ~depth { env } _ state  ->
+    Full(global,{|reads the inductive type declaration for the environment.
+% Supported attributes:
+% - @uinstance! I (default: fresh instance I)|}))),
+  (fun i _ ~depth { env; options } _ state  ->
      let mind, indbo = lookup_inductive env i in
+     let uinst, state, extra_goals = handle_uinst_option_for_inductive ~depth options i state in    
      let knames = CList.(init Declarations.(indbo.mind_nb_constant + indbo.mind_nb_args) (fun k -> GlobRef.ConstructRef(i,k+1))) in
      let k_impls = List.map (fun x -> Impargs.extract_impargs_data (Impargs.implicits_of_global x)) knames in
      let hd x = match x with [] -> [] | (_,x) :: _ -> List.map implicit_kind_of_status x in
      let k_impls = List.map hd k_impls in
      let i_impls = Impargs.extract_impargs_data @@ Impargs.implicits_of_global (GlobRef.IndRef i) in
      let i_impls = hd i_impls in
-     state, !: (fst i, (mind,indbo), (i_impls,k_impls)), [])),
+     state, !: (fst i, uinst, (mind,indbo), (i_impls,k_impls)), extra_goals)),
   DocNext);
 
+  (* TODO: MLCode(Pred("coq.env.indc->indt", *)
+
   MLCode(Pred("coq.env.indc",
     In(constructor, "GR",
     Out(int, "ParamNo",
     Out(int, "UnifParamNo",
     Out(int, "Kno",
     COut(closed_ground_term,"Ty",
-    Full (global, "reads the type Ty of an inductive constructor GR, as well as "^
-          "the number of parameters ParamNo and uniform parameters "^
-          "UnifParamNo and the number of the constructor Kno (0 based)")))))),
-  (fun (i,k as kon) _ _ _ ty ~depth { env } _ state ->
+    Full (global, {|reads the type Ty of an inductive constructor GR, as well as
+the number of parameters ParamNo and uniform parameters
+UnifParamNo and the number of the constructor Kno (0 based).
+Supported attributes:
+- @uinstance! I (default: fresh instance I)|})))))),
+  (fun (i,k as kon) _ _ _ ty ~depth { env; options } _ state ->
     let open Declarations in
     let mind, indbo as ind = Inductive.lookup_mind_specif env i in
     let lno = mind.mind_nparams in
     let luno = mind.mind_nparams_rec in
+    let uinst, state, extra_goals =
+      match options.uinstance with
+      | NoInstance ->
+        if keep ty then
+          let term, ctx =
+            UnivGen.fresh_global_instance (get_global_env state) (GlobRef.ConstructRef kon) in
+          snd @@ Constr.destConstruct term,
+          update_sigma state
+            (fun sigma -> Evd.merge_context_set UState.univ_flexible_alg sigma ctx),
+          []
+        else
+          Univ.Instance.empty, state, []
+      | ConcreteInstance i -> i, state, []
+      | VarInstance (v_head, v_args, v_depth) ->
+        let v' = U.move ~from:v_depth ~to_:depth (E.mkUnifVar v_head ~args:v_args state) in
+        let term, ctx =
+          UnivGen.fresh_global_instance (get_global_env state) (GlobRef.ConstructRef kon) in
+        let uinst = snd @@ Constr.destConstruct term in
+        let state, lp_uinst, extra_goals = uinstance.Conv.embed ~depth state uinst in
+        uinst,
+        update_sigma state
+          (fun sigma -> Evd.merge_context_set UState.univ_flexible_alg sigma ctx),
+        API.Conversion.Unify (v', lp_uinst) :: extra_goals
+    in
     let ty = if_keep ty (fun () ->
-      Inductive.type_of_constructor (kon,Univ.Instance.empty) ind
+      Inductive.type_of_constructor (kon, uinst) ind
       |> EConstr.of_constr) in
-    state, !: lno +! luno +! (k-1) +? ty, [])),
+    state, !: lno +! luno +! (k-1) +? ty, extra_goals)),
   DocAbove);
 
   MLCode(Pred("coq.env.informative?",
@@ -1338,42 +1405,94 @@ regarded as not non-informative).|})),
         | Context.Named.Declaration.LocalDef _ -> raise Pred.No_clause
         | Context.Named.Declaration.LocalAssum _ -> ())),
   DocAbove);
+
+  MLCode(Pred("coq.env.univpoly?",
+  In(gref, "GR",
+  Out(B.int, "PolyArity",
+  Read(global, "checks if GR is universe polymorphic and if so returns the number of universe variables"))),
+    (fun gr _ ~depth {env} _ _ ->
+      if Environ.is_polymorphic env gr then
+        let open Univ.AbstractContext in let open Declareops in let open Environ in
+        match gr with
+        | GlobRef.ConstRef c -> !: (size (constant_polymorphic_context (lookup_constant c env)))
+        | GlobRef.ConstructRef ((i,_),_)
+        | GlobRef.IndRef (i,_) -> !: (size (inductive_polymorphic_context (lookup_mind i env)))
+        | GlobRef.VarRef _ -> assert false
+      else raise No_clause)),
+  DocAbove);
   
   MLCode(Pred("coq.env.const",
     In(constant,  "GR",
     COut(!>> option closed_ground_term, "Bo",
     COut(closed_ground_term, "Ty",
-    Full (global, "reads the type Ty and the body Bo of constant GR. "^
-          "Opaque constants have Bo = none.")))),
-  (fun c bo ty ~depth {env} _ state ->
+    Full (global, {|reads the type Ty and the body Bo of constant GR.
+Opaque constants have Bo = none.
+Supported attributes:
+- @uinstance! I (default: fresh instance I)|})))),
+  (fun c bo ty ~depth { env ; options } _ state ->
+    let type_of_global' state term inst_opt =
+      let state, (ty, inst) = type_of_global state term inst_opt in
+      state, ty, Some inst
+    in
     match c with
     | Constant c ->
-        let state, ty = if_keep_acc ty state (fun s -> type_of_global s (GlobRef.ConstRef c)) in
-        let state, bo = if_keep_acc bo state (fun state ->
-          if Declareops.is_opaque (Environ.lookup_constant c env)
-          then state, None
+      let state, ty_opt, uinst_opt, gl_opt1 =
+        if keep ty then
+          let state, ty, uinst_opt, gls =
+            compute_with_uinstance ~depth options state type_of_global' (GlobRef.ConstRef c) None in
+          state, Some ty, uinst_opt, gls
+        else
+          let uinst_opt =
+            match options.uinstance with
+            | ConcreteInstance i -> Some i
+            | _ -> None
+          in
+          state, None, uinst_opt, []
+      in
+      let state, bo_opt, gl_opt2 =
+        if keep bo then
+          if Declareops.is_opaque (Environ.lookup_constant c env) then
+            state, Some None, []
           else
-            body_of_constant state c) in
-        state, ?: bo +? ty, []
+            let state, bo, _, gls2 =
+              compute_with_uinstance ~depth options state body_of_constant c uinst_opt in
+            state, Some bo, gls2
+        else
+          state, None, []
+      in
+      state, ?: bo_opt +? ty_opt, gl_opt1 @ gl_opt2
     | Variable v ->
-        let state, ty = if_keep_acc ty state (fun s -> type_of_global s (GlobRef.VarRef v)) in
-        let bo = if_keep bo (fun () ->
-          match Environ.lookup_named v env with
-          | Context.Named.Declaration.LocalDef(_,bo,_) -> Some (bo |> EConstr.of_constr)
-          | Context.Named.Declaration.LocalAssum _ -> None) in
-        state, ?: bo +? ty, [])),
+      let state, ty, gls =
+        if keep ty then
+          let state, ty, _, gls =
+            compute_with_uinstance ~depth options state type_of_global' (GlobRef.VarRef v) None in
+          state, Some ty, gls
+        else
+          state, None, []
+      in
+      let bo = if_keep bo (fun () ->
+        match Environ.lookup_named v env with
+        | Context.Named.Declaration.LocalDef(_,bo,_) -> Some (bo |> EConstr.of_constr)
+        | Context.Named.Declaration.LocalAssum _ -> None) in
+      state, ?: bo +? ty, gls)),
   DocAbove);
 
   MLCode(Pred("coq.env.const-body",
     In(constant,  "GR",
     COut(!>> option closed_ground_term, "Bo",
-    Full (global, "reads the body of a constant, even if it is opaque. "^
-          "If such body is none, then the constant is a true axiom"))),
-  (fun c _ ~depth {env} _ state ->
+    Full (global, {|reads the body of a constant, even if it is opaque.
+If such body is none, then the constant is a true axiom.
+Supported attributes:
+- @uinstance! I (default: fresh instance I)|}))),
+  (fun c _ ~depth { env ; options } _ state ->
     match c with
     | Constant c ->
-         let state, bo = body_of_constant state c in
-         state, !: bo, []
+      let state, bo, gls =
+        let state, bo, _, gls =
+          compute_with_uinstance ~depth options state body_of_constant c None in
+        state, bo, gls
+      in
+      state, !: bo, gls
     | Variable v ->
          state, !: begin
          match Environ.lookup_named v env with
@@ -1467,9 +1586,12 @@ regarded as not non-informative).|})),
  
   LPDoc "-- Environment: write -----------------------------------------------";
 
-  LPDoc ("Note: universe constraints are taken from ELPI's constraints "^
+  LPDoc ("Note: (monomorphic) universe constraints are taken from ELPI's constraints "^
          "store. Use coq.univ-* in order to add constraints (or any higher "^
-         "level facility as coq.typecheck)");
+         "level facility as coq.typecheck). Load in the context attributes such as "^
+         "@univpoly!, @univpoly-cumul!, @udecl! or @udecl-cumul! in order to declare "^
+         "universe polymorphic constants or inductives."
+         );
 
   MLCode(Pred("coq.env.add-const",
     In(id,   "Name",
@@ -1486,10 +1608,14 @@ an error. Note: using this API for declaring an axiom or a section variable is
 deprecated, use coq.env.add-axiom or coq.env.add-section-variable instead.
 Supported attributes:
 - @local! (default: false)
-- @using! (default: section variables actually used)|})))))),
+- @using! (default: section variables actually used)
+- @univpoly! (default unset)
+- @udecl! (default unset)
+|})))))),
   (fun id body types opaque _ ~depth {options} _ -> on_global_state "coq.env.add-const" (fun state ->
     let local = options.local = Some true in
-    let sigma = get_sigma state in
+    let state = minimize_universes state in
+    (* Maybe: UState.nf_universes on body and type *)
      match body with
      | B.Unspec -> (* axiom *)
        begin match types with
@@ -1497,10 +1623,11 @@ Supported attributes:
          err Pp.(str "coq.env.add-const: both Type and Body are unspecified")
        | B.Given ty ->
        warn_deprecated_add_axiom ();
-       let gr = add_axiom_or_variable "coq.env.add-const" id sigma ty local options.inline in
+       let gr = add_axiom_or_variable "coq.env.add-const" id ty local options state in
        state, !: (global_constant_of_globref gr), []
      end
     | B.Given body ->
+       let sigma = get_sigma state in
        if not (is_ground sigma body) then
          err Pp.(str"coq.env.add-const: the body must be ground. Did you forge to call coq.typecheck-indt-decl?");
        let opaque = opaque = B.Given true in
@@ -1516,18 +1643,28 @@ Supported attributes:
             if not (is_ground sigma ty) then
               err Pp.(str"coq.env.add-const: the type must be ground. Did you forge to call coq.typecheck-indt-decl?");
              Some ty in
-       let udecl = UState.default_univ_decl in
+       let state, poly, cumul, udecl, _ = poly_cumul_udecl_variance_of_options state options in
+       if cumul then err Pp.(str"coq.env.add-const: unsupported attribute @udecl-cumul! or @univpoly-cumul!");
        let kind = Decls.(IsDefinition Definition) in
        let scope = if local
-         then Locality.Discharge
-         else Locality.(Global ImportDefaultBehavior) in
-       let using = Option.map  Proof_using.(fun s ->
+        then Locality.Discharge
+      else Locality.(Global ImportDefaultBehavior) in
+        let using = Option.map  Proof_using.(fun s ->
+          let sigma = get_sigma state in
           let types = Option.List.cons types [] in
           let using = using_from_string s in
           definition_using (get_global_env state) sigma ~using ~terms:types)
          options.using in
        let cinfo = Declare.CInfo.make ?using ~name:(Id.of_string id) ~typ:types ~impargs:[] () in
-       let info = Declare.Info.make ~scope ~kind ~poly:false ~udecl () in
+       let info = Declare.Info.make ~scope ~kind ~poly ~udecl () in
+
+       let used =
+         Univ.Level.Set.union
+           (universes_of_term state body)
+           (Option.default (EConstr.mkRel 1) types |> universes_of_term state) in
+       let used = Univ.Level.Set.union used (universes_of_udecl state udecl) in
+       let sigma = restricted_sigma_of used state in
+   
        let gr = Declare.declare_definition ~cinfo ~info ~opaque ~body sigma in
        state, !: (global_constant_of_globref gr), []))),
   DocAbove);
@@ -1540,13 +1677,12 @@ Supported attributes:
 and the current module.
 Supported attributes:
 - @local! (default: false)
+- @univpoly! (default unset)
 - @using! (default: section variables actually used)
 - @inline! (default: no inlining)
-- @inline-at! N (default: no inlining)
-|})))),
+- @inline-at! N (default: no inlining)|})))),
   (fun id ty _ ~depth {options} _ -> on_global_state "coq.env.add-axiom" (fun state ->
-     let sigma = get_sigma state in
-     let gr = add_axiom_or_variable "coq.env.add-axiom" id sigma ty false options.inline in
+     let gr = add_axiom_or_variable "coq.env.add-axiom" id ty false options state in
      state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 
@@ -1557,8 +1693,7 @@ Supported attributes:
     Full (global, {|Declare a new section variable: C gets a constant derived from Name
 and the current module|})))),
   (fun id ty _ ~depth {options} _ -> on_global_state "coq.env.add-section-variable" (fun state ->
-     let sigma = get_sigma state in
-     let gr = add_axiom_or_variable "coq.env.add-section-variable" id sigma ty true options.inline in
+     let gr = add_axiom_or_variable "coq.env.add-section-variable" id ty true options state in
      state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 
@@ -1568,12 +1703,18 @@ and the current module|})))),
     Full(global, {|Declares an inductive type.
 Supported attributes:
 - @primitive! (default: false, makes records primitive)|}))),
-  (fun (me, uctx, record_info, ind_impls) _ ~depth env _ -> on_global_state "coq.env.add-indt" (fun state ->
+  (fun (me, uctx, univ_binders, record_info, ind_impls) _ ~depth _ _ -> on_global_state "coq.env.add-indt" (fun state ->
      let sigma = get_sigma state in
      if not (is_mutual_inductive_entry_ground me sigma) then
        err Pp.(str"coq.env.add-indt: the inductive type declaration must be ground. Did you forge to call coq.typecheck-indt-decl?");
      let primitive_expected = match record_info with Some(p, _) -> p | _ -> false in
-     let ubinders = UState.Monomorphic_entry uctx, UnivNames.empty_binders in
+     let ubinders = 
+       let open Entries in
+       match me.mind_entry_universes with
+       | Monomorphic_ind_entry -> (UState.Monomorphic_entry uctx, univ_binders)
+       | Template_ind_entry _ -> nYI "template polymorphic inductives"
+       | Polymorphic_ind_entry uctx -> (UState.Polymorphic_entry uctx, univ_binders)
+       in
      let () = DeclareUctx.declare_universe_context ~poly:false uctx in
      let mind =
        DeclareInd.declare_mutual_inductive_with_eliminations ~primitive_expected me ubinders ind_impls in
@@ -1816,11 +1957,78 @@ denote the same x as before.|};
             Some (c, np + na))))))),
   DocAbove);
 
-  LPDoc "-- Universes --------------------------------------------------------";
-
+  LPDoc "-- Sorts (and their universe level, if applicable) ----------------";
+  LPDoc {|Warning: universe polymorphism has to be considered experimental *E* as
+a feature, not just as a set of APIs. Unfortunately some of the
+current complexity is exposed to the programmer, bare with us.
+
+The big bang is that in Coq one has terms, types and sorts (which are
+the types of types). Some sorts (as of today only Type) some with
+a universe level, on paper Type_i for some i. At the sort level
+Coq features some form of subtyping: a function expecting a function
+to Type, e.g. nat -> Type, can receive a function to Prop, since
+Prop <= Type. So far, so good. But what are these levels i exactly?
+
+Universe levels are said to be "algebraic", they are made of
+variables (see the next section) and the two operators +1 and max.
+This is a sort of internal optimization that leaks to the
+user/programmer. Indeed these universe levels cannot be (directly) used
+in all APIs morally expecting a universe level "i", in particular
+the current constraint engine cannot handle constraint with an
+algebraic level on the right, e.g. i <= j+1. Since some APIs only
+accept universe variables, we provide the coq.univ.variable API
+which is able to craft a universe variable which is roughly
+equivalent to an algebraic universe, e.g. k such that j+1 = k.
+
+Coq-Elpi systematically purges algebraic universes from terms (and
+types and sorts) when one reads them from the environment. This
+makes the embedding of terms less precise than what it could be.
+The different data types stay, since Coq will eventually become
+able to handle algebraic universes consistently, making this purging
+phase unnecessary.|};
   MLData univ;
+  MLData sort;
+
+  MLCode(Pred("coq.sort.leq",
+    InOut(B.ioarg_flex sort, "S1",
+    InOut(B.ioarg_flex sort, "S2",
+    Full(unit_ctx, "constrains S1 <= S2"))),
+  (fun u1 u2 ~depth _ _ state ->
+    match u1, u2 with
+    | Data u1, Data u2 -> add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[]
+    | _ -> err Pp.(str"coq.sort.leq: called with _ as argument"))),
+  DocAbove);
+
+  MLCode(Pred("coq.sort.eq",
+    InOut(B.ioarg_flex sort, "S1",
+    InOut(B.ioarg_flex sort, "S2",
+    Full(unit_ctx, "constrains S1 = S2"))),
+  (fun u1 u2 ~depth _ _ state ->
+    match u1, u2 with
+    | Data u1, Data u2 -> add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, []
+    | _ -> err Pp.(str"coq.sort.eq: called with _ as argument"))),
+  DocAbove);
+
+  MLCode(Pred("coq.sort.sup",
+    InOut(B.ioarg_flex sort, "S1",
+    InOut(B.ioarg_flex sort, "S2",
+    Full(unit_ctx,  "constrains S2 = S1 + 1"))),
+  (fun u1 u2 ~depth _ _ state ->
+    match u1, u2 with
+    | Data u1, Data u2 -> univ_super state u1 u2, !: u1 +! u2, []
+    | _ -> err Pp.(str"coq.sort.sup: called with _ as argument"))),
+  DocAbove);
 
-  MLData universe;
+  MLCode(Pred("coq.sort.pts-triple",
+    InOut(B.ioarg_flex sort, "S1",
+    InOut(B.ioarg_flex sort, "S2",
+    Out(sort, "S3",
+    Full(unit_ctx,  "constrains S3 = sort of product with domain in S1 and codomain in S2")))),
+  (fun u1 u2 _ ~depth _ _ state ->
+    match u1, u2 with
+    | Data u1, Data u2 -> let state, u3 = univ_product state u1 u2 in state, !: u1 +! u2 +! u3, []
+    | _ -> err Pp.(str"coq.sort.pts-triple: called with _ as argument"))),
+    DocAbove);
 
   MLCode(Pred("coq.univ.print",
     Read(unit_ctx,  "prints the set of universe constraints"),
@@ -1832,50 +2040,166 @@ denote the same x as before.|};
     ())),
   DocAbove);
 
-  MLCode(Pred("coq.univ.leq",
-    In(univ, "U1",
-    In(univ, "U2",
-    Full(unit_ctx, "constrains U1 <= U2"))),
-  (fun u1 u2 ~depth _ _ state ->
-    add_universe_constraint state (constraint_leq u1 u2), (),[])),
+  MLCode(Pred("coq.univ.new",
+    Out(univ, "U",
+    Full(unit_ctx, "A fresh universe.")),
+  (fun _ ~depth _ _ state ->
+     let state, (_,u) = new_univ_level_variable state in
+     state, !: u, [])),
   DocAbove);
 
-  MLCode(Pred("coq.univ.eq",
-    In(univ, "U1",
-    In(univ, "U2",
-    Full(unit_ctx, "constrains U1 = U2"))),
-  (fun u1 u2 ~depth _ _ state ->
-    add_universe_constraint state (constraint_eq u1 u2),(), [])),
+  MLCode(Pred("coq.univ",
+    InOut(B.ioarg id, "Name",
+    InOut(B.ioarg univ, "U",
+    Read(unit_ctx, "Finds a named unvierse. Can fail."))),
+  (fun nl u ~depth _ _ state ->
+     match nl, u with
+     | Data nl, _ ->
+         begin try ?: None +! (Univ.Universe.make @@ Evd.universe_of_name (get_sigma state) (Id.of_string_soft nl))
+         with Not_found -> raise No_clause end
+     | _, Data u ->
+         begin match Univ.Universe.level u with
+         | None -> raise Not_found
+         | Some u ->
+            let l = Id.Map.bindings @@ Evd.universe_binders (get_sigma state) in
+            begin try !: (Id.to_string @@ fst @@ List.find (fun (_,u') -> Univ.Level.equal u u') l) +? None
+            with Not_found -> raise No_clause end end
+     | NoData, NoData -> err Pp.(str "coq.univ: both argument were omitted"))),
+  DocAbove);
+
+  MLCode(Pred("coq.univ.global?",
+    In(univ, "U",
+    Easy "succeeds if U is a global universe"),
+  (fun u ~depth ->
+    let global_univs = UGraph.domain (Environ.universes (Global.env ())) in
+    match Univ.Universe.level u with
+    | Some l when Univ.Level.Set.mem l global_univs -> ()
+    | _ -> raise No_clause (* err Pp.(Univ.Universe.pr u ++ str " is not global") *)
+  )),
   DocAbove);
 
-  MLCode(Pred("coq.univ.new",
-    In(B.unspec (list id), "Names",
-    Out(univ, "U",
-    Full(unit_ctx, "fresh universe *E*"))),
-  (fun nl _ ~depth _ _ state ->
-     if not (nl = B.Unspec || nl = B.Given []) then nYI "named universes";
-     let state, u = mk_fresh_univ state in
-     state, !: u, [])),
+  MLCode(Pred("coq.univ.constraints",
+    Out(B.list universe_constraint, "CL",
+    Full(unit_ctx,  "gives the list of constraints, see also coq.univ.variable.constraints")),
+   (fun _ ~depth _ _ state ->
+      let sigma = get_sigma state in
+      let ustate = Evd.evar_universe_context sigma in
+      let constraints = UState.constraints ustate in
+      state, !: (Univ.Constraints.elements constraints), []
+    )),
   DocAbove);
 
-  MLCode(Pred("coq.univ.sup",
-    In(univ, "U1",
-    In(univ, "U2",
-    Full(unit_ctx,  "constrains U2 = U1 + 1"))),
-  (fun u1 u2 ~depth _ _ state ->
-    univ_super state u1 u2, (), [])),
+  LPDoc "-- Universe variables ------";
+
+  MLData universe_level_variable;
+
+  MLCode(Pred("coq.univ.variable",
+    InOut(B.ioarg univ,"U",
+    InOut(B.ioarg universe_level_variable,"L",
+    Full(unit_ctx,  "relates a univ-variable L to a univ U"))),
+  (fun u l ~depth _ _ state ->
+    match u, l with
+    | Data u, NoData ->
+        let state, l, _, _ = force_level_of_universe state u in
+        state, ?: None +! l, []
+    | NoData, Data l ->
+        state, !: (Univ.Universe.make l) +? None, []
+    | NoData, NoData ->
+        let state, (l,u) = new_univ_level_variable state in
+        state, !: u +! l, []
+    | Data u, Data l ->
+      let w = Sorts.sort_of_univ (Univ.Universe.make l) in
+      let state = add_universe_constraint state (constraint_leq (Sorts.sort_of_univ u) w) in
+      state, ?: None +? None, [])),
+  DocAbove);
+
+  MLCode(Pred("coq.univ.variable.constraints",
+    In(universe_level_variable, "L",
+    Out(B.list universe_constraint, "CL",
+    Full(unit_ctx,  "gives the list of constraints on L. Can be used to craft a strict upoly-decl"))),
+   (fun v _ ~depth _ _ state ->
+      let sigma = get_sigma state in
+      let ustate = Evd.evar_universe_context sigma in
+      let constraints = UState.constraints ustate in
+      let v_constraints = Univ.Constraints.filter (fun (l1,_,l2) -> Univ.Level.(equal v l1 || equal v l2)) constraints in
+      state, !: (Univ.Constraints.elements v_constraints), []
+    )),
+  DocAbove);
+ 
+  LPDoc "-- Universe instance (for universe polymorphic global terms) ------";
+
+  LPDoc {|As of today a universe polymorphic constant can only be instantiated
+with universe level variables. That is f@{Prop} is not valid, nor
+is f@{u+1}. One can only write f@{u} for any u.
+
+A univ-instance is morally a list of universe level variables,
+but its list syntax is hidden in the terms. If you really need to
+craft or inspect one of these, the following APIs can help you.
+
+Most of the time the user is expected to use coq.env.global which
+crafts a fresh, appropriate, universe instance and possibly unify that
+term (of the instance it contains) with another one.|};
+
+  MLData uinstance;
+
+  MLCode(Pred("coq.univ-instance",
+    InOut(B.ioarg uinstance, "UI",
+    InOut(B.ioarg (list B.(ioarg_poly "univ-variable")), "UL",
+    Full(global, "relates a univ-instance UI and a list of universe level variables UL"))),
+  (fun uinst_arg univs_arg ~depth { env ; options } _ state ->
+    match uinst_arg, univs_arg with
+    | Data uinst, _ ->
+      let elpi_term_of_level state l =
+        let state, t, gls = universe_level_variable.Conv.embed ~depth state l in
+        assert (gls = []);
+        state, mkData t
+      in
+      let state, univs =
+        CArray.fold_left_map elpi_term_of_level state (Univ.Instance.to_array uinst) in
+      state, ?: None +! Array.to_list univs, []
+    | NoData, Data univs ->
+      let readback_or_new state = function
+        | NoData -> let state, (l,_) = new_univ_level_variable state in state, l, []
+        | Data t -> universe_level_variable.Conv.readback ~depth state t in
+      let state, levels, gls = U.map_acc readback_or_new state univs in
+      state, !: (Univ.Instance.of_array (Array.of_list levels)) +? None, gls
+    | NoData, NoData ->
+      err (Pp.str "coq.univ-instance called with no input argument")
+  )),
   DocAbove);
 
-  MLCode(Pred("coq.univ.pts-triple",
-    In(univ, "U1",
-    In(univ, "U2",
-    Out(univ, "U3",
-    Full(unit_ctx,  "constrains U3 = universe of product with domain in U1 and codomain in U2)")))),
-  (fun u1 u2 _ ~depth _ _ state ->
-    let state, u3 = univ_product state u1 u2 in
-    state, !: u3, [])),
+  MLCode(Pred("coq.univ-instance.unify-eq",
+    In(gref, "GR",
+    In(uinstance, "UI1",
+    In(uinstance, "UI2",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(global, "unifies the two universe instances for the same gref"))))),
+  (fun gr ui1 ui2 diag ~depth { env } _ state ->
+    unify_instances_gref gr ui1 ui2 diag env state EConstr.eq_constr_universes)),
+  DocAbove);
+
+  MLCode(Pred("coq.univ-instance.unify-leq",
+    In(gref, "GR",
+    In(uinstance, "UI1",
+    In(uinstance, "UI2",
+    InOut(B.ioarg B.diagnostic, "Diagnostic",
+    Full(global, "unifies the two universe instances for the same gref. Note: if the GR is not *cumulative* (see Cumulative or #[universes(cumulative)]) then this API imposes an equality constraint."))))),
+  (fun gr ui1 ui2 diag ~depth { env } _ state ->
+    unify_instances_gref gr ui1 ui2 diag env state EConstr.leq_constr_universes)),
   DocAbove);
 
+  LPDoc "-- Declaration of universe polymorphic global terms -----------";
+
+  LPDoc {|These are the data types used to declare how constants
+and inductive types should be declared (see also the @udecl! and
+@udecl-cumul! macros). Note that only inductive types can be
+declared as cumulative.|};
+
+  MLData universe_constraint;
+  MLData universe_variance;
+  MLData universe_decl;
+  MLData universe_decl_cumul;
+
   LPDoc "-- Primitive --------------------------------------------------------";
 
   MLData Coq_elpi_utils.uint63;
@@ -2327,7 +2651,7 @@ Supported attributes:
              let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum(name,ty)) env in
              aux vars nenv env (n-1) t
          | _ ->
-             API.Utils.type_error
+             U.type_error
                (Printf.sprintf "coq.notation.add-abbreviation: term with %d more lambdas expected" n)
          in
          let vars = [] in
@@ -2382,7 +2706,7 @@ Supported attributes:
         | None -> CErrors.anomaly Pp.(str"coq.notation.abbreviation")
       in
         aux ~depth nargs teta in
-    state, !: (API.Utils.beta ~depth t arglist), []
+    state, !: (U.beta ~depth t arglist), []
   )),
   DocAbove);
 
@@ -2486,7 +2810,7 @@ Universe constraints are put in the constraint store.|})))),
 
   MLCode(Pred("coq.typecheck-ty",
     CIn(term,  "Ty",
-    InOut(B.ioarg universe, "U",
+    InOut(B.ioarg sort, "U",
     InOut(B.ioarg B.diagnostic, "Diagnostic",
     Full (proof_context,
 {|typchecks a type Ty returning its universe U. If U is provided, then
@@ -2603,7 +2927,7 @@ hole. Similarly universe levels present in T are disregarded.|}))))),
 
    MLCode(Pred("coq.elaborate-ty-skeleton",
      CIn(term_skeleton,  "T",
-     Out(universe, "U",
+     Out(sort, "U",
      COut(term,  "E",
      InOut(B.ioarg B.diagnostic, "Diagnostic",
      Full (proof_context,{|elabotares T expecting it to be a type of sort U.
@@ -3068,7 +3392,7 @@ Supported attributes:
      let dbname = Coq_elpi_utils.string_split_on_char '.' dbname in
      warn_if_contains_univ_levels ~depth clause;
      let vars = collect_term_variables ~depth clause in
-     let clause = API.Utils.clause_of_term ?name ?graft ~depth loc clause in
+     let clause = U.clause_of_term ?name ?graft ~depth loc clause in
      let local = ctx.options.local = Some true in
      match scope with
      | B.Unspec | B.Given ExecutionSite ->
@@ -3091,6 +3415,10 @@ Supported attributes:
   ] @
   B.ocaml_set ~name:"coq.gref.set" gref (module GRSet) @
   B.ocaml_map ~name:"coq.gref.map" gref (module GRMap) @
+  B.ocaml_set ~name:"coq.univ.set" univ (module UnivSet) @
+  B.ocaml_map ~name:"coq.univ.map" univ (module UnivMap) @
+  B.ocaml_set ~name:"coq.univ-variable.set" universe_level_variable (module UnivLevelSet) @
+  B.ocaml_map ~name:"coq.univ-variable.map" universe_level_variable (module UnivLevelMap) @
   [
   MLData ppbox;
   MLData ppboxes;
diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml
index 603ab5285..60d8dd853 100644
--- a/src/coq_elpi_glob_quotation.ml
+++ b/src/coq_elpi_glob_quotation.ml
@@ -117,6 +117,36 @@ let rec gterm2lp ~depth state x =
       str"gterm2lp: depth=" ++ int depth ++
       str " term=" ++Printer.pr_glob_constr_env (get_global_env state) (get_sigma state) x);
   match (DAst.get x) (*.CAst.v*) with
+  | GRef(GlobRef.ConstRef p,_ul) when Structures.PrimitiveProjections.mem p ->
+      let p = Option.get @@ Structures.PrimitiveProjections.find_opt p in
+      let hd = in_elpi_gr ~depth state (GlobRef.ConstRef (Projection.Repr.constant p)) in
+      state, hd
+  | GRef(gr, ul) when Global.is_polymorphic gr ->
+    begin match ul with
+    | None ->
+      incr type_gen;
+      let state, s =
+        API.RawQuery.mk_Arg state ~name:(Printf.sprintf "univ_inst_%d" !type_gen) ~args:[]
+      in
+      state, in_elpi_poly_gr ~depth state gr s
+    | Some l -> 
+      let sort_name = function
+        | GSProp 
+        | GProp 
+        | GSet -> nYI "f@{Prop}"
+        | GUniv u -> u
+        | GRawUniv u -> assert false (* TODO: nice error *)
+          (* (try Evd.add_global_univ sigma u with UGraph.AlreadyDeclared -> sigma), u *)
+        | GLocalUniv l -> assert false (* TODO: nice error *)
+          (* universe_level_name sigma l  *)
+      in
+      let glob_level = function
+        | UAnonymous {rigid} -> assert false (* TODO: nice error *)
+        | UNamed s -> sort_name s
+      in
+      let l' = List.map glob_level l in
+      state, in_elpi_poly_gr_instance ~depth state gr (Univ.Instance.of_array (Array.of_list l'))
+    end
   | GRef(gr,_ul) -> state, in_elpi_gr ~depth state gr
   | GVar(id) ->
       let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:default_options state, []) (get_ctx state) in
@@ -130,8 +160,8 @@ let rec gterm2lp ~depth state x =
       let state, s = API.RawQuery.mk_Arg state ~name:(Printf.sprintf "type_%d" !type_gen) ~args:[] in
       state, in_elpi_flex_sort s
   | GSort(UNamed u) ->
-    let env = get_global_env state in
-    state, in_elpi_sort (sort env (get_sigma state) u)
+      let env = get_global_env state in
+      in_elpi_sort ~depth state (sort env (get_sigma state) u)
   | GSort(_) -> nYI "(glob)HOAS for Type@{i j}"
 
   | GProd(name,_,s,t) ->
diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml
index 823150667..078277fd0 100644
--- a/src/coq_elpi_utils.ml
+++ b/src/coq_elpi_utils.ml
@@ -116,8 +116,6 @@ let lookup_inductive env i =
   let mind, indbo = Inductive.lookup_mind_specif env i in
   if Array.length mind.Declarations.mind_packets <> 1 then
     nYI "API(env) mutual inductive";
-  if Declareops.inductive_is_polymorphic mind then
-    nYI "API(env) poly mutual inductive";
   mind, indbo
 
 
@@ -250,3 +248,21 @@ let option_map_acc2 f s = function
 let option_default f = function
   | Some x -> x
   | None -> f ()
+
+let coq_version_parser version =
+  let (!!) x = try int_of_string x with Failure _ -> -100 in
+  match Str.split (Str.regexp_string ".") version with
+  | major :: minor :: patch :: _ -> !!major, !!minor, !!patch
+  | [ major ] -> !!major,0,0
+  | [] -> 0,0,0
+  | [ major; minor ] ->
+      match Str.split (Str.regexp_string "+") minor with
+      | [ minor ] -> !!major, !!minor, 0
+      | [ ] -> !!major, !!minor, 0
+      | minor :: prerelease :: _ ->
+          if Str.string_match (Str.regexp_string "beta") prerelease 0 then
+            !!major, !!minor, !!("-"^String.sub prerelease 4 (String.length prerelease - 4))
+          else if Str.string_match (Str.regexp_string "alpha") prerelease 0 then
+            !!major, !!minor, !!("-"^String.sub prerelease 5 (String.length prerelease - 5))
+          else !!major, !!minor, -100
+
diff --git a/src/coq_elpi_utils.mli b/src/coq_elpi_utils.mli
index 4b70d2050..a8ebb3224 100644
--- a/src/coq_elpi_utils.mli
+++ b/src/coq_elpi_utils.mli
@@ -54,3 +54,5 @@ val pp_qualified_name : Format.formatter -> qualified_name -> unit
 val option_map_acc : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option
 val option_map_acc2 : (Elpi.API.State.t -> 'b -> Elpi.API.State.t * 'c * Elpi.API.Conversion.extra_goals) -> Elpi.API.State.t -> 'b option -> Elpi.API.State.t * 'c option * Elpi.API.Conversion.extra_goals
 val option_default : (unit -> 'a) -> 'a option -> 'a
+
+val coq_version_parser : string -> int * int * int
diff --git a/tests/test_API.v b/tests/test_API.v
index 433e7e2fa..b01122799 100644
--- a/tests/test_API.v
+++ b/tests/test_API.v
@@ -71,11 +71,11 @@ Elpi Query lp:{{ std.do! [
 (***** Univs *******************************)
 
 Elpi Query lp:{{coq.univ.print}}.
-Elpi Query lp:{{coq.univ.new [] X}}.
-Elpi Query lp:{{coq.univ.leq X Y}}.
-Elpi Query lp:{{coq.univ.eq X Y}}.
-Elpi Query lp:{{coq.univ.pts-triple X Y Z}}.
-Elpi Query lp:{{coq.univ.sup X Y}}.
+Elpi Query lp:{{coq.univ.new X}}.
+Elpi Query lp:{{coq.sort.leq X Y}}.
+Elpi Query lp:{{coq.sort.eq X Y}}.
+Elpi Query lp:{{coq.sort.pts-triple X Y Z}}.
+Elpi Query lp:{{coq.sort.sup X Y}}.
 
 
 (********* accumulate *************** *)
diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v
index 6fed5bf8f..485acc556 100644
--- a/tests/test_API_elaborate.v
+++ b/tests/test_API_elaborate.v
@@ -55,8 +55,10 @@ Elpi Command test.API2.
 Elpi Accumulate lp:{{
   main [indt-decl D] :- coq.say "raw:" D,
     std.assert-ok! (coq.elaborate-indt-decl-skeleton D D1) "illtyped",
+    coq.say "elab1:" D1,
     coq.env.add-indt D1 I,
-    coq.env.indt-decl I D2, coq.say "elab:" D2.
+    coq.env.indt-decl I D2,
+    coq.say "elab2:" D2.
   main [const-decl N (some BO) TYA] :- std.do! [
     coq.arity->term TYA TY,
     std.assert-ok! (coq.elaborate-ty-skeleton TY _ TY1) "illtyped",
diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v
index 6d35228f9..6048ecbe5 100644
--- a/tests/test_HOAS.v
+++ b/tests/test_HOAS.v
@@ -56,7 +56,7 @@ End kwd.
 
 Elpi Query lp:{{
   coq.env.begin-section "xxxxx",
-  coq.univ.new [] U,
+  coq.univ.new U,
   T = sort (typ U),
   coq.env.add-section-variable "a" T _,
   coq.env.end-section
@@ -66,7 +66,7 @@ Elpi Db univs.db lp:{{ pred u o:univ. }}.
 Elpi Command test_u.
 Elpi Accumulate Db univs.db.
 Fail Elpi Query lp:{{
-  coq.univ.new [] U,
+  coq.univ.new U,
   coq.elpi.accumulate current "univs.db" (clause _ _ (u U))
 }}.
 
@@ -185,3 +185,348 @@ Elpi Query lp:{{
   coq.locate "nat" {{:gref lib:elpi.test.nat }}.
 
 }}.
+
+Polymorphic Definition toto (T1 T2 : Type) (x : T1) := x.
+Polymorphic Definition titi := toto.
+
+Elpi Query lp:{{
+  coq.locate "titi" (const C),
+  coq.env.const C Body Term,
+  coq.say Body,
+  coq.say Term.
+}}.
+
+Universes u1 u2.
+
+Elpi Query lp:{{
+  coq.say {{ toto }},         % pglobal (const «toto») X
+  coq.say {{ toto@{u1 u2} }}, % pglobal (const «toto») «u1 u2»
+  coq.say {coq.term->string {{ toto }}}.
+}}.
+
+Polymorphic Record F (T : Type) := Build_F { t : T }.
+Polymorphic Definition fnat : F nat := {| t := 0%nat |}.
+
+Elpi Query lp:{{
+  T = {{ @t nat fnat }},
+  coq.say T,
+  coq.typecheck T Ty ok,
+  coq.say T.
+}}.
+
+Section UPolyVar.
+
+Polymorphic Variable n : nat.
+
+Elpi Query lp:{{
+  coq.locate "F" GRF,
+  coq.typecheck (pglobal GRF I) TyF ok,
+  GRF = indt Ind,
+
+  % coq.env.indt
+  @uinstance! I => coq.env.indt Ind _ _ _ Arity K KTys,
+  @uinstance! I => coq.env.indt Ind _ _ _ Arity K _,
+  @uinstance! I => coq.env.indt Ind _ _ _ _ K KTys,
+  @uinstance! I => coq.env.indt Ind _ _ _ _ K _,
+  @uinstance! I => coq.env.indt Ind _ _ _ _ _ _,
+
+  @uinstance! _ => coq.env.indt Ind _ _ _ Arity1 K KTys1,
+  @uinstance! _ => coq.env.indt Ind _ _ _ Arity2 K _,
+  @uinstance! _ => coq.env.indt Ind _ _ _ _ K KTys3,
+  @uinstance! _ => coq.env.indt Ind _ _ _ _ K _,
+  @uinstance! _ => coq.env.indt Ind _ _ _ _ _ _,
+
+  @uinstance! A4 => coq.env.indt Ind _ _ _ Arity4 K KTys4,
+  @uinstance! A5 => coq.env.indt Ind _ _ _ Arity5 K _,
+  @uinstance! A6 => coq.env.indt Ind _ _ _ _ K KTys6,
+  @uinstance! A7 => coq.env.indt Ind _ _ _ _ K _,
+  @uinstance! A8 => coq.env.indt Ind _ _ _ _ _ _,
+
+  @uinstance! A4 => coq.env.indt Ind _ _ _ Arity4 K KTys4,
+  @uinstance! A5 => coq.env.indt Ind _ _ _ Arity5 K _,
+  @uinstance! A6 => coq.env.indt Ind _ _ _ _ K KTys6,
+
+  coq.locate "Build_F" GRB,
+  coq.typecheck (pglobal GRB I2) TyB ok,
+  GRB = indc B,
+
+  % coq.env.indc
+  @uinstance! I2 => coq.env.indc B _ _ _ TyB,
+  @uinstance! I2 => coq.env.indc B _ _ _ _,
+
+  @uinstance! _ => coq.env.indc B _ _ _ BTy2,
+  @uinstance! _ => coq.env.indc B _ _ _ _,
+
+  @uinstance! B1 => coq.env.indc B _ _ _ BTy3,
+  @uinstance! B2 => coq.env.indc B _ _ _ _,
+
+  @uinstance! B1 => coq.env.indc B _ _ _ BTy3,
+
+  coq.locate "t" GRt,
+  coq.typecheck (pglobal GRt I3) Tyt ok,
+  GRt = const T,
+
+  % coq.env.const
+  % constant
+  @uinstance! I3 => coq.env.const T BoT TyT,
+  @uinstance! I3 => coq.env.const T BoT _,
+  @uinstance! I3 => coq.env.const T _ TyT,
+  @uinstance! I3 => coq.env.const T _ _,
+
+  @uinstance! _ => coq.env.const T BoT1 TyT1,
+  @uinstance! _ => coq.env.const T BoT2 _,
+  @uinstance! _ => coq.env.const T _ TyT3,
+  @uinstance! _ => coq.env.const T _ _,
+
+  @uinstance! D1 => coq.env.const T BoT4 TyT4,
+  @uinstance! D2 => coq.env.const T BoT5 _,
+  @uinstance! D3 => coq.env.const T _ TyT5,
+  @uinstance! D4 => coq.env.const T _ _,
+
+  @uinstance! D1 => coq.env.const T BoT4 TyT4,
+  @uinstance! D2 => coq.env.const T BoT5 _,
+  @uinstance! D3 => coq.env.const T _ TyT5,
+
+  coq.locate "n" GRn,
+  GRn = const N,
+
+  % variable (non polymorphic)
+  @uinstance! _ => coq.env.const N BoN TyN,
+  @uinstance! _ => coq.env.const N BoN _,
+  @uinstance! _ => coq.env.const N _ TyN,
+  @uinstance! _ => coq.env.const N _ _,
+
+  @uinstance! I4 => coq.env.const N BoN TyN,
+  @uinstance! I4 => coq.env.const N BoN _,
+  @uinstance! I4 => coq.env.const N _ TyN,
+  @uinstance! I4 => coq.env.const N _ _,
+
+  % coq.env.typeof
+  % indt
+  @uinstance! I => coq.env.typeof GRF TyF,
+  @uinstance! I => coq.env.typeof GRF _,
+
+  @uinstance! _ => coq.env.typeof GRF TyF2,
+  @uinstance! _ => coq.env.typeof GRF _,
+
+  @uinstance! C1 => coq.env.typeof GRF TyF3,
+  @uinstance! C2 => coq.env.typeof GRF _,
+
+  @uinstance! C1 => coq.env.typeof GRF TyF3,
+
+  % indc
+  @uinstance! I2 => coq.env.typeof GRB TyB,
+  @uinstance! I2 => coq.env.typeof GRB _,
+
+  @uinstance! _ => coq.env.typeof GRB TyB2,
+  @uinstance! _ => coq.env.typeof GRB _,
+
+  @uinstance! C3 => coq.env.typeof GRB TyB3,
+  @uinstance! C4 => coq.env.typeof GRB _,
+
+  @uinstance! C3 => coq.env.typeof GRB TyB3,
+
+  % const
+  @uinstance! I3 => coq.env.typeof GRt TyT,
+  @uinstance! I3 => coq.env.typeof GRt _,
+
+  @uinstance! _ => coq.env.typeof GRt TyT6,
+  @uinstance! _ => coq.env.typeof GRt _,
+
+  @uinstance! C5 => coq.env.typeof GRt TyT7,
+  @uinstance! C6 => coq.env.typeof GRt _,
+
+  @uinstance! C5 => coq.env.typeof GRt TyT7,
+
+  % var
+  @uinstance! I4 => coq.env.typeof GRn TyN,
+  @uinstance! I4 => coq.env.typeof GRn _,
+
+  @uinstance! _ => coq.env.typeof GRn TyN,
+  @uinstance! _ => coq.env.typeof GRn _,
+
+  % coq.env.const-body
+  % const
+  @uinstance! I3 => coq.env.const-body T BoT,
+  @uinstance! I3 => coq.env.const-body T _,
+
+  @uinstance! _ => coq.env.const-body T BoT6,
+  @uinstance! _ => coq.env.const-body T _,
+
+  @uinstance! E5 => coq.env.const-body T BoT7,
+  @uinstance! E6 => coq.env.const-body T _,
+
+  @uinstance! E5 => coq.env.const-body T BoT7,
+
+  % var
+  @uinstance! I4 => coq.env.const-body N BoN,
+  @uinstance! I4 => coq.env.const-body N _,
+  
+  @uinstance! _ => coq.env.const-body N BoN,
+  @uinstance! _ => coq.env.const-body N _.
+}}.
+
+Elpi Query lp:{{
+  coq.locate "F" GRF,
+  GRF = indt Ind,
+
+  % coq.env.indt
+  @uinstance! I => coq.env.indt-decl Ind Decl,
+  coq.say I Decl,
+  @uinstance! I => coq.env.indt-decl Ind Decl1,
+  coq.say I Decl1,
+
+  @uinstance! _ => coq.env.indt-decl Ind Decl2,
+  coq.say Decl2.
+
+}}.
+
+End UPolyVar.
+
+Elpi Query lp:{{
+  coq.locate "F" GRF,
+  coq.typecheck (pglobal GRF I1) _ ok,
+  coq.typecheck (pglobal GRF I2) _ ok,
+  coq.say I1 I2,
+  coq.univ.print,
+  coq.univ-instance.unify-eq GRF I1 I2 ok,
+  coq.univ.print.
+}}.
+
+Elpi Query lp:{{
+  coq.locate "F" GRF,
+  coq.locate "fnat" GRfnat,
+  coq.typecheck (pglobal GRF I1) _ ok,
+  coq.typecheck (pglobal GRfnat I2) _ ok,
+  coq.say I1 I2,
+  coq.univ.print,
+  coq.univ-instance.unify-eq GRF I1 I2 (error E),
+  coq.say E,
+  coq.univ.print.
+}}.
+
+Elpi Query lp:{{
+  coq.locate "F" GRF,
+  coq.typecheck (pglobal GRF I1) _ ok,
+  coq.univ-instance I1 UL1,
+  coq.univ-instance I1 [U],
+  coq.univ-instance I2 [U].
+}}.
+
+Elpi Query lp:{{
+  coq.locate "F" GRF,
+  coq.typecheck (pglobal GRF I1) _ ok,
+  coq.typecheck (pglobal GRF I2) _ ok,
+  coq.univ-instance I1 [L1],
+  coq.univ-instance I2 [L2],
+  coq.univ.variable U1 L1,
+  coq.univ.variable U2 L2,
+  coq.sort.sup (typ U1) (typ U2),
+  coq.univ-instance.unify-eq GRF I1 I2 (error E),
+  coq.say E.
+}}.
+
+Cumulative Polymorphic Record F2@{+x} (T : Type@{x}) := Build_F2 { t2 : T }.
+
+Elpi Query lp:{{
+  coq.locate "F2" GRF,
+  coq.typecheck (pglobal GRF I1) _ ok,
+  coq.typecheck (pglobal GRF I2) _ ok,
+  coq.univ-instance I1 [L1],
+  coq.univ-instance I2 [L2],
+  coq.univ.variable U1 L1,
+  coq.univ.variable U2 L2,
+  coq.sort.sup (typ U1) (typ U2),
+  coq.univ.print,
+  coq.univ-instance.unify-leq GRF I1 I2 ok. % why does this add a = not a <= ?
+}}.
+
+Elpi Query lp:{{
+  coq.locate "F" GRF,
+  coq.env.global GRF (pglobal GRF I1),
+  coq.typecheck (pglobal GRF I2) _ ok,
+  coq.univ-instance I1 [L1],
+  coq.univ-instance I2 [L2],
+  coq.univ.variable U1 L1,
+  coq.univ.variable U2 L2,
+  coq.sort.sup (typ U1) (typ U2),
+  coq.univ.print,
+  coq.univ-instance.unify-leq GRF I2 I1 (error E),
+  coq.say E.
+}}.
+
+Elpi Query lp:{{
+  coq.locate "nat" GR,
+  coq.env.global GR (global GR)
+}}.
+
+Elpi Query lp:{{
+  coq.locate "F" GR,
+  coq.env.global GR (pglobal GR I)
+}}.
+
+
+Elpi Query lp:{{
+  coq.locate "F" GR,
+  not(coq.env.global GR (global GR))
+}}.
+
+Elpi Query lp:{{
+  coq.locate "F" GR,
+  @uinstance! I => coq.say {coq.env.global GR},
+  coq.locate "Build_F" GR1,
+  coq.say I,
+  @uinstance! I => coq.say {coq.env.global GR1}.
+
+}}.
+
+Elpi Query lp:{{
+  coq.univ-instance I [U,U],
+  coq.say I
+}}.
+
+
+(*
+
+#[universes(polymorphic)]
+Definition poly@{x y | x < y } : Type@{y} := Type@{x}.
+Set Printing Universes.
+About poly.
+
+#[universes(polymorphic)]
+Inductive Box@{x y z} : Type@{z} := K : (Type@{x} -> Type@{y}) -> (Type@{y} -> Type@{x}) -> Box.
+Set Printing Universes.
+About Box.
+*)
+
+Elpi Query lp:{{
+  
+  Body = (sort (typ UX)),
+  Type = (sort (typ UY)),
+  coq.univ.print,
+  coq.say "------------------",
+  coq.typecheck Body Type ok,
+  coq.univ.print,
+
+  coq.univ.variable UX LX,
+  coq.univ.variable UY LY,
+  coq.univ.print,
+
+  @udecl! [LX,LY] ff [lt LX LY] ff =>
+    coq.env.add-const "poly" Body Type _ _.
+
+/*
+  @udecl-cumul! [invariant UX,auto UY,covar UZ| _] _ =>
+    coq.env.add-indt (inductive "Box" tt (arity (sort (typ UZ))) i\[
+      constructor "K" (arity
+        prod `_` (prod `_` (sort (typ UX)) (_\sort (typ UY))) _\
+        prod `_` (prod `_` (sort (typ UY)) (_\sort (typ UX))) _\
+        i)
+    ]) _.
+*/
+}}.
+
+Set Printing Universes.
+About poly.
+Check poly@{Set Type}.
+About Box.
diff --git a/tests/test_arg_HOAS.v b/tests/test_arg_HOAS.v
index 4a3c07eba..7c830b0bd 100644
--- a/tests/test_arg_HOAS.v
+++ b/tests/test_arg_HOAS.v
@@ -10,14 +10,32 @@ main [indt-decl A] :- !,
   std.assert-ok! (coq.typecheck-indt-decl A) "Illtyped inductive declaration",
   coq.say "typed:" A,
   coq.env.add-indt A _.
+main [upoly-indt-decl A UD] :- !,
+  coq.say "raw:" A UD,
+  coq.univ.print,
+  std.assert-ok! (coq.typecheck-indt-decl A) "Illtyped inductive declaration",
+  coq.say "typed:" A,
+  coq.upoly-decl->attribute UD CL,
+  CL => coq.env.add-indt A _.
 main [const-decl N (some BO) A] :- !,
   coq.arity->term A TY,
   std.assert-ok! (coq.typecheck BO TY) "illtyped definition",
   coq.env.add-const N BO TY _ _.
+ main [upoly-const-decl N (some BO) A UD] :- !,
+  coq.arity->term A TY,
+  std.assert-ok! (coq.typecheck BO TY) "illtyped definition",
+  coq.upoly-decl->attribute UD CL,
+  CL => coq.env.add-const N BO TY _ _.
 main [const-decl N none A] :- !,
   coq.arity->term A TY,
   std.assert-ok! (coq.typecheck-ty TY _) "illtyped axiom",
   coq.env.add-axiom N TY _.
+main [upoly-const-decl N none A UD] :- !,
+  coq.arity->term A TY,
+  std.assert-ok! (coq.typecheck-ty TY _) "illtyped axiom",
+  coq.upoly-decl->attribute UD CL,
+  CL => coq.env.add-axiom N TY _.
+
 main [ctx-decl (context-item "T" _ _ none t\
                 context-item "x" _ t none _\
                 context-item "l" _ _ (some _) _\
@@ -36,15 +54,34 @@ main [indt-decl RA] :- !,
   std.assert-ok! (coq.elaborate-indt-decl-skeleton RA A) "Illtyped inductive declaration",
   coq.say "typed:" A,
   coq.env.add-indt A _.
+main [upoly-indt-decl RA UD] :- !,
+  coq.say "raw:" RA UD,
+  coq.univ.print,
+  std.assert-ok! (coq.elaborate-indt-decl-skeleton RA A) "Illtyped inductive declaration",
+  coq.say "typed:" A,
+  coq.upoly-decl->attribute UD CL,
+  CL => coq.env.add-indt A _.
 main [const-decl N (some RBO) RA] :- !,
   coq.arity->term RA RTY,
   std.assert-ok! (coq.elaborate-ty-skeleton RTY _ TY) "illtyped arity", 
   std.assert-ok! (coq.elaborate-skeleton RBO TY BO) "illtyped definition",
   coq.env.add-const N BO TY _ _.
+main [upoly-const-decl N (some RBO) RA UD] :- !,
+  coq.arity->term RA RTY,
+  std.assert-ok! (coq.elaborate-ty-skeleton RTY _ TY) "illtyped arity", 
+  std.assert-ok! (coq.elaborate-skeleton RBO TY BO) "illtyped definition",
+  coq.upoly-decl->attribute UD CL,
+  CL => coq.env.add-const N BO TY _ _.
 main [const-decl N none RA] :- !,
   coq.arity->term RA RTY,
   std.assert-ok! (coq.elaborate-ty-skeleton RTY _ TY) "illtyped axiom",
   coq.env.add-axiom N TY _.
+main [upoly-const-decl N none RA UD] :- !,
+  coq.arity->term RA RTY,
+  std.assert-ok! (coq.elaborate-ty-skeleton RTY _ TY) "illtyped axiom",
+  coq.upoly-decl->attribute UD CL,
+  CL => coq.env.add-axiom N TY _.
+
 main [ctx-decl (context-item "T" _ _ none t\
                 context-item "x" _ t none _\
                 context-item "l" _ _ (some _) _\
@@ -134,7 +171,7 @@ End raw_record_attributes.
 (*****************************************)
 
 Module definition.
-Elpi declarations
+Elpi Trace. Elpi declarations
 Definition x1 (P : Type) (w : P) (n : nat) := (n + 1).
 Check x1 : forall P, P -> nat -> nat.
 Check refl_equal _ : x1 = fun P w n => n + 1.
@@ -205,4 +242,48 @@ Elpi Query lp:{{
 }}.
 
 Print r.
-End copy.
\ No newline at end of file
+End copy.
+
+Set Printing Universes.
+
+(*****************************************)
+
+Elpi declarations #[universes(template=no)] Inductive X1 : Type := .
+Fail Elpi declarations #[universes(template)] Inductive X2 : Type := .
+About X1.
+
+Fail Elpi Query lp:{{ coq.locate "X1" GR, coq.env.global GR (pglobal GR _) }}.
+
+(*****************************************)
+
+Elpi declarations #[universes(polymorphic)] Inductive X3 : Type := .
+Elpi declarations #[universes(polymorphic,cumulative)] Inductive X4 : Type := .
+About X3.
+About X4.
+
+Elpi Query lp:{{ coq.locate "X3" GR, coq.env.global GR (pglobal GR _) }}.
+Elpi Query lp:{{ coq.locate "X4" GR, coq.env.global GR (pglobal GR _) }}.
+
+Elpi declarations #[universes(polymorphic)] Inductive X5@{u} : Type@{u} := .
+About X5.
+
+Elpi declarations #[universes(polymorphic)] Inductive X6@{u v|u<v} : Type@{v} := K (u : Type@{u}).
+About X6.
+
+Fail Elpi raw_declarations #[universes(polymorphic)] Inductive X7@{u v|u<v} : Type@{v} := K (u : Type@{u}).
+
+Elpi raw_declarations #[universes(polymorphic)] Inductive X8 : Type := .
+About X8.
+
+(* ******************** *)
+Elpi declarations #[universes(polymorphic)] Definition f1 (T:Type) (x:T) := x.
+About f1.
+
+Elpi declarations #[universes(polymorphic)] Definition f2@{u} (T:Type@{u}) (T1:Type@{u}) (x:T) := x.
+About f2.
+
+Elpi raw_declarations #[universes(polymorphic)] Definition f3 (T:Type) (x:T) := x.
+About f3.
+
+Elpi raw_declarations #[universes(polymorphic)] Definition f4@{u} (T:Type@{u}) (T1:Type@{u}) (x:T) := x.
+About f4.