diff --git a/.nix/config.nix b/.nix/config.nix
index 79f6812fb..56f25a953 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -1,5 +1,7 @@
-with builtins; with (import <nixpkgs> {}).lib;
-let master = [
+with builtins;
+with (import <nixpkgs> { }).lib;
+let
+  master = [
     "coqeal"
     "hierarchy-builder"
     "mathcomp"
@@ -11,9 +13,10 @@ let master = [
     "multinomials"
     "odd-order"
   ];
-  common-bundles = listToAttrs (forEach master (p:
-    { name = p; value.override.version = "master"; }))
-  // {
+  common-bundles = listToAttrs (forEach master (p: {
+    name = p;
+    value.override.version = "master";
+  })) // {
     coq-elpi-tests.job = true;
     stdlib.job = true;
     coq-elpi-tests-stdlib.job = true;
@@ -25,12 +28,12 @@ let master = [
 
     deriving.job = false;
     reglang.job = false;
-}; in
-{
+  };
+in {
   format = "1.0.0";
   attribute = "rocq-elpi";
   coq-attribute = "coq-elpi";
-  default-bundle = "coq-8.20";
+  default-bundle = "rocq-master";
   bundles = {
 
     "coq-8.20".coqPackages = common-bundles // {
@@ -44,36 +47,40 @@ let master = [
       coq-elpi.override.elpi-version = "2.0.7";
     };
 
-    "coq-master" = { rocqPackages = {
-      rocq-core.override.version = "master";
-      rocq-elpi.override.elpi-version = "2.0.7";
-      stdlib.override.version = "master";
-      bignums.override.version = "master";
-    }; coqPackages = common-bundles // {
-      coq.override.version = "master";
-      coq-elpi.override.elpi-version = "2.0.7";
-      stdlib.override.version = "master";
-      bignums.override.version = "master";
-    }; };
-      
+    "rocq-master" = {
+      rocqPackages = {
+        rocq-core.override.version = "mattam82:universes-clauses";
+        rocq-elpi.override.elpi-version = "2.0.7";
+        stdlib.override.version = "master";
+        bignums.override.version = "master";
+      };
+      coqPackages = common-bundles // {
+        coq.override.version = "mattam82:universes-clauses";
+        coq-elpi.override.elpi-version = "2.0.7";
+        stdlib.override.version = "master";
+        bignums.override.version = "master";
+      };
+    };
+
     /* uncomment bundle below if min and max elpi version start to differ
-    "coq-master-min-elpi" = { rocqPackages = {
-      rocq-core.override.version = "master";
-      rocq-elpi.override.elpi-version = "2.0.7";
-      stdlib.override.version = "master";
-      bignums.override.version = "master";
-    }; coqPackages = common-bundles // {
-      coq.override.version = "master";
-      coq-elpi.override.elpi-version = "2.0.7";
-      stdlib.override.version = "master";
-      bignums.override.version = "master";
-    }; }; */
+       "coq-master-min-elpi" = { rocqPackages = {
+         rocq-core.override.version = "master";
+         rocq-elpi.override.elpi-version = "2.0.7";
+         stdlib.override.version = "master";
+         bignums.override.version = "master";
+       }; coqPackages = common-bundles // {
+         coq.override.version = "master";
+         coq-elpi.override.elpi-version = "2.0.7";
+         stdlib.override.version = "master";
+         bignums.override.version = "master";
+       }; };
+    */
 
   };
 
-  cachix.coq = {};
-  cachix.math-comp = {};
-  cachix.coq-community = {};
+  cachix.coq = { };
+  cachix.math-comp = { };
+  cachix.coq-community = { };
   cachix.coq-elpi.authToken = "CACHIX_AUTH_TOKEN";
 
 }
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi
index cc545f4f4..7822b6605 100644
--- a/builtin-doc/coq-builtin.elpi
+++ b/builtin-doc/coq-builtin.elpi
@@ -789,6 +789,7 @@ external pred coq.env.current-section-path o:list string.
 % - @using! (default: section variables actually used)
 % - @univpoly! (default unset)
 % - @udecl! (default unset)
+% - @udecl-cumul! (default unset)
 % - @dropunivs! (default: false, drops all universe constraints from the
 % store after the definition)
 % 
@@ -995,7 +996,7 @@ 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.
+external pred coq.sort.pts-triple i:sort, i:sort, o:sort.
 
 % [coq.univ.print] prints the set of universe constraints
 external pred coq.univ.print .
@@ -1040,11 +1041,9 @@ external pred coq.univ.variable.of-term i:term, o:coq.univ.variable.set.
 
 % -- 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 universe polymorphic constant can be instantiated with universes.
 % 
-% A univ-instance is morally a list of universe level variables,
+% A univ-instance is morally a list of universes,
 % 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.
 % 
@@ -1080,11 +1079,10 @@ external pred coq.univ-instance.unify-leq i:gref, i:univ-instance,
 % @udecl-cumul! macros). Note that only inductive types can be
 % declared as cumulative.
 
-% Constraint between two universes level variables
+% Constraint between two universes
 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.
+type le univ -> univ -> univ-constraint.
+type eq univ -> univ -> univ-constraint.
 
 % Variance of a universe level variable
 kind univ-variance type.
@@ -1093,8 +1091,8 @@ 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 +})
+% Constraints for a polymorphic 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.
diff --git a/coq-elpi.opam b/coq-elpi.opam
index c80409da4..6913c2055 100644
--- a/coq-elpi.opam
+++ b/coq-elpi.opam
@@ -1,3 +1,4 @@
+version: "2.5.2-45-gca1b82d"
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis: "Compatibility metapackage for Elpi extension language after the Rocq renaming"
diff --git a/dune-project b/dune-project
index bdecff756..773d06b93 100644
--- a/dune-project
+++ b/dune-project
@@ -1,6 +1,7 @@
 (lang dune 3.13)
 (using coq 0.8)
 (name rocq-elpi)
+(version v2.5.2-45-gca1b82d)
 ;(generate_opam_files)
 
 (source (github LPCIC/coq-elpi))
diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi
index ebdcdbbbc..498d39dca 100644
--- a/elpi/coq-lib.elpi
+++ b/elpi/coq-lib.elpi
@@ -210,7 +210,6 @@ coq.upoly-decl-cumul.complete-constraints.aux (covariant V) CS :- coq.univ.varia
 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.
 
diff --git a/rocq-elpi.opam b/rocq-elpi.opam
index 53c7bd8b5..b5d521773 100644
--- a/rocq-elpi.opam
+++ b/rocq-elpi.opam
@@ -1,3 +1,4 @@
+version: "2.5.2-45-gca1b82d"
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis: "Elpi extension language for Coq"
diff --git a/src/rocq_elpi_HOAS.ml b/src/rocq_elpi_HOAS.ml
index 57780ca2d..aa7cb2aab 100644
--- a/src/rocq_elpi_HOAS.ml
+++ b/src/rocq_elpi_HOAS.ml
@@ -127,10 +127,10 @@ let add_universe_constraint state c =
       Feedback.msg_debug Pp.(str"UniversesDiffer");
       raise API.BuiltInPredicate.No_clause
 
-let new_univ_level_variable ?(flexible=false) state =
+let new_univ_level_variable ?(flexible=true) 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 rigidity = if flexible then UState.univ_flexible_alg else UState.univ_rigid in
+    let rigidity = if flexible then UState.univ_flexible else UState.univ_rigid in
     let sigma, v = Evd.new_univ_level_variable ?name:None rigidity sigma in
     let u = Univ.Universe.make v in
     (*
@@ -207,16 +207,13 @@ let universe_level_variable =
 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";
+  doc = "Constraint between two universes";
   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)),
+    K("le","",A(univ,A(univ,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)),
+    K("eq","",A(univ,A(univ,N)),
       B (fun u1 u2 -> (u1,Univ.Eq,u2)),
       M (fun ~ok ~ko -> function (l1,Univ.Eq,l2) -> ok l1 l2 | _ -> ko ()))
   ]
@@ -243,33 +240,60 @@ let universe_variance : (Univ.Level.t * UVars.Variance.t option) API.Conversion.
   ]
 } |> 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 {
+let universe_decl : UState.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
+  let open UState 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 +})";
+  doc = "Constraints for a polymorphic 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))
+     B (fun x sx y sy -> 
+      { univdecl_qualities = []; univdecl_extensible_qualities = false; 
+        univdecl_instance = x; univdecl_extensible_instance = sx; 
+        univdecl_variances = None; 
+        univdecl_constraints = Univ.Constraints.of_list y;
+        univdecl_extensible_constraints = sy }),
+     M (fun ~ok ~ko:_ x -> 
+      ok x.univdecl_instance x.univdecl_extensible_instance
+        (Univ.Constraints.elements x.univdecl_constraints) 
+        x.univdecl_extensible_constraints))
   ]
 } |> API.ContextualConversion.(!<)
 
-type universe_decl_cumul = ((Univ.Level.t * UVars.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 {
+let universe_decl_cumul : UState.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 
+  let open UState 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))
+     B (fun x sx y sy -> 
+      { univdecl_qualities = []; univdecl_extensible_qualities = false; 
+        univdecl_instance = List.map fst x; univdecl_extensible_instance = sx; 
+        univdecl_variances = Some (Array.of_list (List.map snd x)); 
+        univdecl_constraints = Univ.Constraints.of_list y;
+        univdecl_extensible_constraints = sy }),
+     M (fun ~ok ~ko:_ x ->       
+      ok (List.map2 (fun x y -> x, y) x.univdecl_instance (Array.to_list (Option.get x.univdecl_variances))) 
+      x.univdecl_extensible_instance
+        (Univ.Constraints.elements x.univdecl_constraints)
+        x.univdecl_extensible_constraints))
   ]
 } |> API.ContextualConversion.(!<)
 
+let collapse_to_type_sigma sigma s =
+  match s with
+  | Sorts.QSort (q, u) ->
+    let sigma = Evd.set_eq_qualities sigma (Sorts.Quality.QVar q) Sorts.Quality.qtype in
+    sigma, Sorts.make Sorts.Quality.qtype u
+  | x -> sigma, s
 
+let collapse_to_type_state state s = 
+    S.update_return (Option.get !pre_engine) state (fun ({ sigma } as x) ->
+      let sigma, s = collapse_to_type_sigma sigma s in
+      { x with sigma }, s)
 
 (* All in one data structure to represent the Coq context and its link with
    the elpi one:
@@ -298,8 +322,8 @@ type uinstanceoption =
     (* 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
+  | Cumulative of UState.universe_decl
+  | NonCumulative of UState.universe_decl
 type options = {
   hoas_holes : hole_mapping option;
   local : bool option;
@@ -336,7 +360,7 @@ let default_options () = {
   keepunivs = None;
   redflags = None;
   no_tc = None;
-  algunivs = None;
+  algunivs = Some true;
 }
 let make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth
   ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs
@@ -400,6 +424,7 @@ let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversi
     | Sorts.SProp -> Format.fprintf fmt "SProp"
     | Sorts.QSort _ -> Format.fprintf fmt "QSort");
   embed = (fun ~depth { options } _ state s ->
+    let state, s = collapse_to_type_state state s in
     match s with
     | Sorts.Prop -> state, E.mkConst propc, []
     | Sorts.SProp -> state, E.mkConst spropc, []
@@ -409,7 +434,7 @@ let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversi
     | Sorts.Type u ->
         let state, u, gls = univ.embed ~depth state u in
         state, E.mkApp typc u [], gls
-    | Sorts.QSort _ -> nYI "sort polymorphism");
+    | Sorts.QSort (q, u) -> nYI ("sort polymorphism: " ^ Sorts.QVar.to_string q));
   readback = (fun ~depth { options } _ state t ->
     match E.look ~depth t with
     | E.Const c when c == propc -> state, Sorts.prop, []
@@ -526,14 +551,14 @@ let constructorina ~loc x = A.mkOpaque ~loc (constructorino x)
 let compare_instances x y =
   let qx, ux = UVars.Instance.to_array x
   and qy, uy = UVars.Instance.to_array y in
-  Util.Compare.(compare [(CArray.compare Sorts.Quality.compare, qx, qy); (CArray.compare Univ.Level.compare, ux, uy)])
+  Util.Compare.(compare [(CArray.compare Sorts.Quality.compare, qx, qy); (CArray.compare Univ.Universe.compare, ux, uy)])
 
 let uinstancein, uinstanceino, isuinstance, uinstanceout, uinstance =
   let { CD.cin; cino; isc; cout }, uinstance = CD.declare {
     CD.name = "univ-instance";
     doc = "Universes level instance for a universe-polymorphic constant";
     pp = (fun fmt x ->
-      let s = Pp.string_of_ppcmds (UVars.Instance.pr Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes x) in
+      let s = Pp.string_of_ppcmds (UVars.Instance.pr Sorts.QVar.raw_pr (Univ.Universe.pr UnivNames.pr_level_with_global_universes) x) in
       Format.fprintf fmt "«%s»" s);
     compare = compare_instances;
     hash = UVars.Instance.hash;
@@ -668,12 +693,15 @@ let in_elpiast_gr ~loc r =
   assert_in_elpi_gref_consistent ~poly:false r;
   A.mkAppGlobal ~loc globalc (in_elpiast_gref ~loc r) []
 
+let in_elpi_pglobal t i =
+  E.mkApp pglobalc t [i]
+
 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]
+  in_elpi_pglobal t i
 
 let in_elpiast_poly_gr ~loc r i =
   assert_in_elpi_gref_consistent ~poly:true r;
@@ -1073,6 +1101,9 @@ let force_level_of_universe state u =
       let w = Sorts.sort_of_univ v in
       add_universe_constraint state (constraint_eq (Sorts.sort_of_univ u) w), l, v, w
 
+[%%if coq = "9.2"]
+let purge_algebraic_univs_sort state s = state, EConstr.ESorts.kind (S.get engine state).sigma s
+[%%else]
 let purge_algebraic_univs_sort state s =
   let sigma = (S.get engine state).sigma in
   match EConstr.ESorts.kind sigma s with
@@ -1080,6 +1111,12 @@ let purge_algebraic_univs_sort state s =
       let state, _, _, s = force_level_of_universe state u in
       state, s
   | x -> state, x
+[%%endif]
+
+let collapse_to_type state s =
+  S.update_return engine state (fun ({ sigma } as e) -> 
+    let sigma, s = collapse_to_type_sigma sigma s in
+    { e with sigma }, s)
 
 let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []
 let in_elpiast_flex_sort ~loc t =
@@ -1090,7 +1127,9 @@ let sort = { sort with API.ContextualConversion.embed = (fun ~depth ctx csts sta
     if ctx.options.algunivs = None || ctx.options.algunivs = Some false then
       purge_algebraic_univs_sort state (EConstr.ESorts.make s)
     else
-      state, s in
+      let state, s = collapse_to_type state s in
+      state, s
+  in
   sort.API.ContextualConversion.embed ~depth ctx csts state s) }
 
 let in_elpi_sort ~depth ctx csts state s =
@@ -1108,6 +1147,9 @@ let in_elpiast_sort ~loc state s =
 
 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 update_return_sigma s f = 
+  (S.update_return engine s (fun e -> let sigma, r = f e.sigma in 
+   { e with sigma }, r))
 let get_global_env s = (S.get engine s).global_env
 
 let declare_evc = E.Constants.declare_global_symbol "declare-evar"
@@ -1700,7 +1742,6 @@ let body_of_constant state c inst_opt = S.update_return engine state (fun x ->
      let sigma = match priv with
      | Opaqueproof.PrivateMonomorphic () -> sigma
      | Opaqueproof.PrivatePolymorphic ctx ->
-      let ctx = Util.on_snd (Univ.subst_univs_level_constraints (snd (UVars.make_instance_subst inst))) ctx in
       Evd.merge_context_set Evd.univ_rigid sigma ctx
      in
      { x with sigma }, (Some (EConstr.of_constr bo), Some inst)
@@ -1715,10 +1756,9 @@ let evar_arity k state =
                    u < FOO.123
    even if u is a binder, and FOO.123 is not.
    Hence this is disabled. *)
-let minimize_universes state = state (*
+let minimize_universes 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
@@ -1840,8 +1880,8 @@ let analyze_scope ~depth coq_ctx args =
 module UIM = F.Map(struct
   type t = UVars.Instance.t
   let compare = compare_instances
-  let show x = Pp.string_of_ppcmds @@ UVars.Instance.pr Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes x
-  let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (UVars.Instance.pr Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes x)
+  let show x = Pp.string_of_ppcmds @@ UVars.Instance.pr Sorts.QVar.raw_pr (Univ.Universe.pr UnivNames.pr_level_with_global_universes) x
+  let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (UVars.Instance.pr Sorts.QVar.raw_pr (Univ.Universe.pr UnivNames.pr_level_with_global_universes) x)
 end)
     
 let uim = S.declare_component ~name:"rocq-elpi:evar-univ-instance-map" ~descriptor:interp_state
@@ -1858,7 +1898,7 @@ let in_coq_poly_gref ~depth ~origin ~failsafe s t i =
         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_sort_context_set UState.univ_flexible_alg sigma ctx) in
+        let s = update_sigma s (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx) in
         let u =
           match C.kind u with
           | C.Const (_, u) -> u
@@ -1869,7 +1909,11 @@ let in_coq_poly_gref ~depth ~origin ~failsafe s t i =
         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
+    | _ ->
+      let s, ri, extra = uinstance.readback ~depth s i in
+      let sigma = get_sigma s in
+      let eri = EConstr.EInstance.make ri in
+      s, EConstr.EInstance.kind sigma eri, extra
   in
   try
     let s, t, gls1 = gref.readback ~depth s t in
@@ -2930,7 +2974,7 @@ let restricted_sigma_of s state =
   let sigma = get_sigma state in
   let ustate = Evd.evar_universe_context sigma in
   let ustate = UState.restrict_even_binders ustate s in
-  let ustate = UState.fix_undefined_variables ustate in
+  (* let ustate = UState.fix_undefined_variables ustate in *)
   let ustate = UState.collapse_sort_variables ustate in
   let sigma = Evd.set_universe_context sigma ustate in
   sigma
@@ -2943,7 +2987,7 @@ let universes_of_udecl state ({ UState.univdecl_instance ; univdecl_constraints
   let used1 = 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
+  let used = List.fold_right (fun x acc -> Univ.Level.Set.union (Univ.Universe.levels x) acc) (List.flatten used2) used in
   used
 
 let name_universe_level = ref 0
@@ -2961,7 +3005,7 @@ let name_universe_level state l =
         { e with sigma }, id
   )
 
-
+[%%if coq = "9.2"]
 let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance =
   let open UState in
   { univdecl_qualities = [];
@@ -2969,22 +3013,24 @@ let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraint
     univdecl_extensible_qualities = false;
     univdecl_extensible_constraints;
     univdecl_constraints;
-    univdecl_instance}
+    univdecl_variances = None;
+    univdecl_instance; }
+[%%else]
+let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance =
+  let open UState in
+  { univdecl_qualities = [];
+    univdecl_extensible_instance;
+    univdecl_extensible_qualities = false;
+    univdecl_extensible_constraints;
+    univdecl_constraints;
+    univdecl_instance; }
+[%%endif]
 
 let poly_cumul_udecl_variance_of_options state options =
   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 univdecl_instance, variance = List.split univ_lvlt_var in
-    state, true, true,
-    mk_universe_decl 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 univdecl_instance = univ_lvlt in
-    let variance = List.init (List.length univdecl_instance) (fun _ -> None) in
-    state, true, false,
-    mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance,
-    Array.of_list variance
+  | NotUniversePolymorphic -> state, false, false, UState.default_univ_decl, None
+  | Cumulative udecl -> state, true, true, udecl, None
+  | NonCumulative udecl -> state, true, false, udecl, None
 
 [%%if coq = "8.20"]
 let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~finite =
@@ -3000,6 +3046,20 @@ let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~fin
   }
   in
   ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags
+[%%elif coq = "9.2"]
+let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~finite ~udecl ~variances =
+  let flags = {
+    ComInductive.poly;
+    cumulative;
+    template = Some false;
+    finite;
+    mode = None;
+  }
+  in
+  let udecl = 
+    UState.{ udecl with univdecl_variances = variances }
+  in
+  ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags ~udecl
 [%%else]
 let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~finite ~ctx_params ~env_ar_params =
   let flags = {
@@ -3011,7 +3071,8 @@ let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~fin
   }
   in
   let env_ar = Environ.pop_rel_context (List.length ctx_params) env_ar_params in
-  ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags ~env_ar ~ctx_params
+  ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags 
+    ~env_ar ~ctx_params
 [%%endif]
 
 
@@ -3100,9 +3161,8 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
         let open Context.Rel.Declaration in
         LocalAssum(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
-
-    (* restruction to used universes *)
-    let state = minimize_universes state in
+    (* restriction to used universes *)
+    
     let used =
       List.fold_left (fun acc t ->
           Univ.Level.Set.union acc
@@ -3487,25 +3547,37 @@ let inductive_decl2lp ~depth coq_ctx constraints state (mutind,uinst,(mind,ind),
   hoas_ind2lp ~depth coq_ctx state ind
 ;;
        
+let udecl_of_entry vars csts variances loose_udecl =
+  let open UState in
+  let of_variances variances =  
+    let variances = UVars.Variances.repr variances in
+    let variances = Array.map (fun v -> Some (UVars.VarianceOccurrence.typing_variances v)) variances in
+    variances
+  in
+  { univdecl_qualities = []; univdecl_extensible_qualities = loose_udecl; 
+    univdecl_instance = vars; univdecl_extensible_instance = loose_udecl;
+    univdecl_variances = Option.map of_variances variances;
+    univdecl_constraints = csts; univdecl_extensible_constraints = loose_udecl }
+
 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 qvars, vars = UVars.Instance.to_array @@ UVars.UContext.instance uc in
+  | Polymorphic_ind_entry (uc, variances) ->
+    let qvars, vars = UVars.LevelInstance.to_array @@ UVars.UContext.instance uc in
     if not (CArray.is_empty qvars) then nYI "sort poly inductives"
     else
       let state, vars = CArray.fold_left_map (fun s l -> fst (name_universe_level s l), l) state vars in
       let csts = UVars.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
+      begin match variances with
+      | None | Some Infer_variances ->
+        let udecl = udecl_of_entry (Array.to_list vars) csts None loose_udecl in
+          let state, up, gls = universe_decl.API.Conversion.embed ~depth state udecl in          
           state, (fun i -> E.mkApp uideclc i [up]), gls
+      | Some (Check_variances variance) ->
+        let udecl = udecl_of_entry (Array.to_list vars) csts (Some variance) loose_udecl in
+        let state, up, gls = universe_decl_cumul.API.Conversion.embed ~depth state udecl in
+        state, (fun i -> E.mkApp uideclc i [up]), gls
       end
   | Monomorphic_ind_entry -> state, (fun i -> E.mkApp ideclc i []), []
 
@@ -3528,7 +3600,7 @@ let inductive_entry2lp ~depth coq_ctx constraints state ~loose_udecl e =
   let state = match mie.mind_entry_universes with
     | Template_ind_entry _ -> nYI "template polymorphic inductives"
     | Monomorphic_ind_entry -> state
-    | Polymorphic_ind_entry cs -> S.update engine state (fun e ->
+    | Polymorphic_ind_entry (cs, _variances) -> S.update engine state (fun e ->
         { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma (snd (UVars.UContext.to_context_set 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
@@ -3584,7 +3656,7 @@ let record_entry2lp ~depth coq_ctx constraints state ~loose_udecl e =
   let state = match mie.mind_entry_universes with
     | Template_ind_entry _ -> nYI "template polymorphic inductives"
     | Monomorphic_ind_entry -> state
-    | Polymorphic_ind_entry cs -> S.update engine state (fun e ->
+    | Polymorphic_ind_entry (cs, _variances) -> S.update engine state (fun e ->
       { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma (snd (UVars.UContext.to_context_set cs)) }) (* ???? *) in
   
   let state, upoly_decl_of, upoly_decl_gls = upoly_decl_of ~depth state ~loose_udecl mie in
@@ -3653,7 +3725,7 @@ let record_entry2lp ~depth coq_ctx constraints state ~loose_udecl (decl:Record.R
   let state = match mie.mind_entry_universes with
     | Template_ind_entry _ -> nYI "template polymorphic inductives"
     | Monomorphic_ind_entry -> state
-    | Polymorphic_ind_entry cs -> S.update engine state (fun e ->
+    | Polymorphic_ind_entry (cs, _variances) -> S.update engine state (fun e ->
       { e with sigma = Evd.merge_context_set UState.univ_flexible e.sigma (snd (UVars.UContext.to_context_set cs)) }) (* ???? *) in
 
   let state, upoly_decl_of, upoly_decl_gls = upoly_decl_of ~depth state ~loose_udecl mie in
diff --git a/src/rocq_elpi_HOAS.mli b/src/rocq_elpi_HOAS.mli
index 5a936f062..a1754ed00 100644
--- a/src/rocq_elpi_HOAS.mli
+++ b/src/rocq_elpi_HOAS.mli
@@ -24,12 +24,10 @@ type uinstanceoption =
   | 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 * UVars.Variance.t option) list  * bool) * (Univ.Constraints.t * bool)
 type universe_decl_option =
   | NotUniversePolymorphic
-  | Cumulative of universe_decl_cumul
-  | NonCumulative of universe_decl
+  | Cumulative of UState.universe_decl
+  | NonCumulative of UState.universe_decl
 
 type options = {
   hoas_holes : hole_mapping option;
@@ -169,6 +167,7 @@ val in_elpi_appl : depth:int -> term -> term list -> term
 val in_elpi_match : term -> term -> term list -> term
 val in_elpi_fix : Name.t -> int -> term -> term -> term
 val in_elpi_name : Name.t -> term
+val in_elpi_pglobal : term -> term -> term
 
 val set_coq : Elpi.API.Ast.Scope.language -> unit
 
@@ -223,8 +222,8 @@ val uinstance : UVars.Instance.t Conversion.t
 
 val universe_constraint : Univ.univ_constraint Conversion.t
 val universe_variance : (Univ.Level.t * UVars.Variance.t option) Conversion.t
-val universe_decl : universe_decl Conversion.t
-val universe_decl_cumul : universe_decl_cumul Conversion.t
+val universe_decl : UState.universe_decl Conversion.t
+val universe_decl_cumul : UState.universe_decl 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
@@ -248,6 +247,8 @@ 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 -> Univ.Universe.t
+val isuinstance : RawOpaqueData.t -> bool
+val uinstanceout : RawOpaqueData.t -> UVars.Instance.t
 
 val is_sort : depth:int -> term -> bool
 val is_prod : depth:int -> term -> (term * term) option (* ty, bo @ depth+1 *)
@@ -317,6 +318,7 @@ val mk_def :
 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
+val update_return_sigma : State.t -> (Evd.evar_map -> Evd.evar_map * 'a) -> State.t * 'a
 
 type hyp = { ctx_entry : term; depth : int }
 
@@ -344,7 +346,7 @@ val force_level_of_universe : state -> Univ.Universe.t -> state * Univ.Level.t *
 val purge_algebraic_univs_sort : state -> EConstr.ESorts.t -> state * 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 poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.universe_decl * UVars.Variance.t option array option
 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
diff --git a/src/rocq_elpi_arg_HOAS.ml b/src/rocq_elpi_arg_HOAS.ml
index 57710a207..256823f63 100644
--- a/src/rocq_elpi_arg_HOAS.ml
+++ b/src/rocq_elpi_arg_HOAS.ml
@@ -90,6 +90,7 @@ type raw_record_decl_elpi = {
   constructor : Names.Id.t option;
   fields : (Vernacexpr.local_decl_expr * Record.Data.projection_flags * Vernacexpr.notation_declaration list) list;
   univpoly : univpoly;
+  univdecl : Constrexpr.cumul_univ_decl_expr option;
 }
 [%%endif]
 type glob_record_decl_elpi = {
@@ -99,6 +100,7 @@ type glob_record_decl_elpi = {
   arity : Glob_term.glob_constr;
   fields : (Glob_term.glob_constr * Rocq_elpi_HOAS.record_field_spec) list;
   univpoly : univpoly;
+  univdecl : Constrexpr.cumul_univ_decl_expr option;
 }
 
 let pr_raw_record_decl _ _ _ = Pp.str "TODO: pr_raw_record_decl"
@@ -113,6 +115,7 @@ type raw_indt_decl_elpi = {
   arity : Constrexpr.constr_expr option;
   constructors : (Names.lident * Constrexpr.constr_expr) list;
   univpoly : univpoly;
+  univdecl : Constrexpr.cumul_univ_decl_expr option;
 }
 type glob_indt_decl_elpi = {
   finiteness : Declarations.recursivity_kind;
@@ -123,6 +126,7 @@ type glob_indt_decl_elpi = {
   nuparams_given : bool;
   constructors : (Names.Id.t * Glob_term.glob_constr) list;
   univpoly : univpoly;
+  univdecl : Constrexpr.cumul_univ_decl_expr option;
 }
 
 let pr_raw_indt_decl _ _ _ = Pp.str "TODO: pr_raw_indt_decl"
@@ -262,7 +266,6 @@ let of_coq_inductive_definition id =
           constructors in
   let { ComInductive.template; 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 = finite;
     name;
@@ -270,7 +273,8 @@ let of_coq_inductive_definition id =
     non_uniform_parameters;
     arity;
     constructors;
-    univpoly = univpoly_of ~poly ~cumulative
+    univpoly = univpoly_of ~poly ~cumulative;
+    univdecl = udecl;
   }
 [%%endif]
 
@@ -312,15 +316,15 @@ let of_coq_record_definition id =
     | Constrexpr.CSort s -> s
     | _ -> CErrors.user_err ?loc:sort.CAst.loc Pp.(str "only explicits sorts are supported")) in
   let { ComInductive.template; 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";
+  if template <> None then nYI "raw template polymorphic inductives";  
   {
     name;
     parameters = binders;
     sort;
     constructor = Some idbuild.v;
     fields = cfs;
-    univpoly = univpoly_of ~poly ~cumulative
+    univpoly = univpoly_of ~poly ~cumulative;
+    univdecl = udecl
   } 
 [%%endif]
 let intern_record_decl glob_sign (it : raw_record_decl) = glob_sign, it
@@ -328,7 +332,11 @@ let intern_record_decl glob_sign (it : raw_record_decl) = glob_sign, it
 let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,None,y,z)
 let dest_entry (_,_,_,_,x) = x
 
+[%%if coq = "9.2"]
+let expr_Type_sort = Constrexpr_ops.expr_Type_sort UState.univ_flexible
+[%%else]
 let expr_Type_sort = Constrexpr_ops.expr_Type_sort
+[%%endif]
 
 [%%if coq = "8.20" || coq = "9.0"]
 let raw_record_decl_to_glob_synterp ({ name; sort; parameters; constructor; fields; univpoly } : raw_record_decl_elpi) : glob_record_decl_elpi =
@@ -379,7 +387,7 @@ let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fi
         (glob_sign_params,intern_env,[]) fields in
   { name = (space, Names.Id.of_string name); arity; params; constructorname = constructor; fields = List.rev fields; univpoly }
 [%%else]
-let raw_record_decl_to_glob_synterp ({ name; sort; parameters; constructor; fields; univpoly } : raw_record_decl_elpi) : glob_record_decl_elpi =
+let raw_record_decl_to_glob_synterp ({ name; sort; parameters; constructor; fields; univpoly; univdecl } : raw_record_decl_elpi) : glob_record_decl_elpi =
   let name, space = sep_last_qualid name in
   let params = intern_global_context_synterp parameters in
   let params = List.rev params in
@@ -401,9 +409,11 @@ let raw_record_decl_to_glob_synterp ({ name; sort; parameters; constructor; fiel
         (x, atts) :: acc
     | Vernacexpr.DefExpr _, _, _ -> Rocq_elpi_utils.nYI "DefExpr")
         [] fields in
-  { name = (space, Names.Id.of_string name); arity; params; constructorname = constructor; fields = List.rev fields; univpoly }
+  { name = (space, Names.Id.of_string name); arity; params; 
+    constructorname = constructor; fields = List.rev fields; 
+    univpoly; univdecl }
 
-let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fields; univpoly } : raw_record_decl_elpi) : glob_record_decl_elpi =
+let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fields; univpoly; univdecl } : 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
@@ -430,10 +440,11 @@ let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fi
         gs, intern_env, (x, atts) :: acc
     | Vernacexpr.DefExpr _, _, _ -> Rocq_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; univpoly }
+  { name = (space, Names.Id.of_string name); arity; params; constructorname = constructor; fields = List.rev fields; 
+    univpoly; univdecl }
 [%%endif]
 
-let raw_indt_decl_to_glob_synterp ({ finiteness; name; parameters; non_uniform_parameters; arity; constructors; univpoly } : raw_indt_decl_elpi) : glob_indt_decl_elpi =
+let raw_indt_decl_to_glob_synterp ({ finiteness; name; parameters; non_uniform_parameters; arity; constructors; univpoly; univdecl } : 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 params = intern_global_context_synterp parameters in
@@ -446,9 +457,9 @@ let raw_indt_decl_to_glob_synterp ({ finiteness; name; parameters; non_uniform_p
   let nuparams = List.rev nuparams in
   let arity = mkGHole in
   let constructors = List.map (fun (id,ty) -> id.CAst.v, mkGHole) constructors in
-  { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly }
+  { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly; univdecl }
   
-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 raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform_parameters; arity; constructors; univpoly; univdecl } : 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
@@ -473,7 +484,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 ~expty:(Pretyping.OfType indty) glob_sign_params_self ~intern_env ty) constructors in
-  { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly }
+  { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly; univdecl }
 let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it
 
 let expr_hole = CAst.make @@ Constrexpr.CHole(None)
@@ -502,14 +513,13 @@ let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); bod
     match udecl, poly with
     | None, false -> state, NotUniversePolymorphic
     | Some _, false -> nYI "only universe polymorphic definitions can take universe binders"
-    | None, true -> state, NonCumulative (([],true),(Univ.Constraints.empty,true))
-    | Some udecl, true ->
+    | _, true ->     
         let open UState in
-        let sigma,  { univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints; univdecl_instance} =
-          Constrintern.interp_univ_decl_opt (Rocq_elpi_HOAS.get_global_env state) (Some udecl) in
+        let sigma, udecl =
+          Constrintern.interp_univ_decl_opt (Rocq_elpi_HOAS.get_global_env state) udecl in
         let ustate = Evd.evar_universe_context sigma in
         let state = merge_universe_context state ustate in
-        state, NonCumulative ((univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in
+        state, NonCumulative udecl in
   let sigma = get_sigma state in
   match body, typ with
   | Some body, _ ->
@@ -540,7 +550,7 @@ let raw_constant_decl_to_glob_synterp ({ name; atts; udecl; typ = (params,typ);
     let open Attributes in
     parse polymorphic atts in
   let udecl =
-    if poly then NonCumulative (([],true),(Univ.Constraints.empty,true))
+    if poly then NonCumulative UState.default_univ_decl
     else NotUniversePolymorphic in
   state, { name = raw_decl_name_to_glob name; params; typ; udecl; body }
   
@@ -558,14 +568,12 @@ let raw_constant_decl_to_glob glob_sign ({ name; atts; udecl; typ = (params,typ)
     match udecl, poly with
     | None, false -> state, NotUniversePolymorphic
     | Some _, false -> nYI "only universe polymorphic definitions can take universe binders"
-    | None, true -> state, NonCumulative (([],true),(Univ.Constraints.empty,true))
-    | Some udecl, true ->
+    | _, true ->
         let open UState in
-        let sigma,  { univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints; univdecl_instance} =
-          Constrintern.interp_univ_decl_opt (Rocq_elpi_HOAS.get_global_env state) (Some udecl) in
+        let sigma, udecl = Constrintern.interp_univ_decl_opt (Rocq_elpi_HOAS.get_global_env state) udecl in
         let ustate = Evd.evar_universe_context sigma in
         let state = merge_universe_context state ustate in
-        state, NonCumulative ((univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in
+        state, NonCumulative udecl 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
 
@@ -716,15 +724,26 @@ let wit = add_genarg "elpi_ftactic_arg"
 
 end
 
-let mk_indt_decl state univpoly r =
+let mk_indt_decl state univpoly ?univdecl r =
+  let state, udecl = 
+    match univdecl with 
+    | None -> state, UState.default_univ_decl
+    | Some univdecl ->
+      let env = get_global_env state in
+      update_return_sigma state
+        (fun sigma -> 
+          let sigma', udecl = Constrintern.interp_cumul_univ_decl_opt env (Some univdecl) in
+          let ustate = Evd.ustate sigma' in
+          Evd.merge_universe_context sigma ustate, udecl)
+  in
   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
+      let state, up, gls = universe_decl.API.Conversion.embed ~depth:0 state udecl 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
+      let state, up, gls = universe_decl.API.Conversion.embed ~depth:0 state udecl in
       assert(gls=[]);
       state, E.mkApp uideclc r [up]
 
@@ -762,10 +781,10 @@ let grecord2lp_synterp ~depth state { Cmd.name; arity; params; constructorname;
   let state, r = gparams2lp_synterp ~depth params (grecord2lp_synterp ~depth ~name ~constructorname arity fields) state in
   mk_indt_decl state univpoly r
       
-let grecord2lp ~loc ~base ~depth state { Cmd.name; arity; params; constructorname; fields; univpoly } =
+let grecord2lp ~loc ~base ~depth state { Cmd.name; arity; params; constructorname; fields; univpoly; univdecl } =
   let open Rocq_elpi_glob_quotation in
   let state, r = gparams2lp ~loc ~base params ~k:(grecord2lp ~loc ~base ~name ~constructorname arity fields) ~depth state in
-  mk_indt_decl state univpoly r
+  mk_indt_decl state univpoly ?univdecl r
   
 let contract_params env sigma name params nuparams_given t =
   if nuparams_given then t else
@@ -807,7 +826,7 @@ let drop_unit f ~depth state =
   let state, x, () = f ~depth state in
   state, x
   
-let ginductive2lp_synterp ~depth state { Cmd.finiteness; name; arity; params; nuparams; nuparams_given; constructors; univpoly } =
+let ginductive2lp_synterp ~depth state { Cmd.finiteness; name; arity; params; nuparams; nuparams_given; constructors; univpoly; univdecl } =
   let space, indt_name = name in
   let nuparams = List.map drop_relevance nuparams in
   let params = List.map drop_relevance params in
@@ -822,9 +841,9 @@ let ginductive2lp_synterp ~depth state { Cmd.finiteness; name; arity; params; nu
     state, in_elpi_indtdecl_inductive state finiteness (Name.Name qindt_name) arity constructors
   in
   let state, r = gparams2lp_synterp params (do_inductive_synterp ~depth) ~depth state in
-  mk_indt_decl state univpoly r
+  mk_indt_decl state univpoly ?univdecl r
   
-let ginductive2lp ~loc ~depth ~base state { Cmd.finiteness; name; arity; params; nuparams; nuparams_given; constructors; univpoly } =
+let ginductive2lp ~loc ~depth ~base state { Cmd.finiteness; name; arity; params; nuparams; nuparams_given; constructors; univpoly; univdecl } =
   let open Rocq_elpi_glob_quotation in
   let space, indt_name = name in
   let contract state x =
@@ -845,7 +864,7 @@ let ginductive2lp ~loc ~depth ~base state { Cmd.finiteness; name; arity; params;
     ~depth state
   in
   let state, r = gparams2lp ~loc ~base params ~k:(drop_unit do_inductive) ~depth state in
-  mk_indt_decl state univpoly r
+  mk_indt_decl state univpoly ?univdecl r
 
 let in_option = Elpi.(Builtin.option API.BuiltInData.any).API.Conversion.embed
 
diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml
index 5ec63e02c..1c86d6cd7 100644
--- a/src/rocq_elpi_builtins.ml
+++ b/src/rocq_elpi_builtins.ml
@@ -164,6 +164,7 @@ let mk_algebraic_super x = Sorts.super x
 
 (* I don't want the user to even know that algebraic universes exist *)
 
+[%%if coq = "8.20" || coq = "9.0" || coq = "9.1" ]
 let univ_super state u v =
   let state, u = match u with
   | Sorts.Set | Sorts.Prop | Sorts.SProp -> state, u
@@ -172,8 +173,13 @@ let univ_super state u v =
     else
       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)
+      add_universe_constraint state (constraint_leq u w), w 
+  in
+  add_universe_constraint state (constraint_leq (mk_algebraic_super u) v)
+[%%else]
+let univ_super state u v =
+  add_universe_constraint state (constraint_eq (mk_algebraic_super u) v)
+[%%endif]
 
 let univ_product state s1 s2 =
   let s = Typeops.sort_of_product (get_global_env state) s1 s2 in
@@ -314,7 +320,7 @@ 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_sort_context_set UState.univ_flexible_alg sigma ctx) in
+      let state = update_sigma state (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx) in
       snd @@ Constr.destInd term, state, []
   | ConcreteInstance i -> i, state, []
   | VarInstance (v_head, v_args, v_depth) ->
@@ -323,7 +329,7 @@ let handle_uinst_option_for_inductive ~depth options i state =
         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_sort_context_set UState.univ_flexible_alg sigma ctx) in
+      let state = update_sigma state (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx) in
       uinst, state, API.Conversion.Unify (v', lp_uinst) :: extra_goals
 
 (* FIXME PARTIAL API
@@ -532,33 +538,49 @@ let err_if_contains_alg_univ ~depth t =
     match Univ.Universe.level u with
     | None -> true
     | Some l -> is_global_level env l in
-  let rec aux ~depth acc t =
+  let rec aux ~depth (acc,acci) t =
     match E.look ~depth t with
+    | E.App _ as x ->
+      begin match is_global_or_pglobal ~depth t with
+      | PGlobal(Some _, Some _) ->(acc,(1+acci))
+      | _ -> Rocq_elpi_utils.fold_elpi_term aux (acc,acci) ~depth x
+      end
+    | E.CData c when isuinstance c ->
+        err Pp.(strbrk "The hypothetical clause contains terms of universe instance")
     | E.CData c when isuniv c ->
         let u = univout c in
-        if is_global u then acc
+        if is_global u then acc, acci
         else
           begin match Univ.Universe.level u with
           | None ->
             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: " ++
               Univ.Universe.pr UnivNames.pr_level_with_global_universes u)
-          | _ -> Univ.Universe.Set.add u acc
+          | _ -> Univ.Universe.Set.add u acc, acci
           end
-    | x -> Rocq_elpi_utils.fold_elpi_term aux acc ~depth x
+    | x -> Rocq_elpi_utils.fold_elpi_term aux (acc,acci) ~depth x
   in
-  let univs = aux ~depth Univ.Universe.Set.empty t in
+  let univs = aux ~depth (Univ.Universe.Set.empty,0) t in
   univs
   
+let coq_env_globalc   = E.Constants.declare_global_symbol "coq.env.global"
+
 let preprocess_clause ~depth clause =
-  let levels_to_abstract = err_if_contains_alg_univ ~depth clause in
-  let levels_to_abstract_no = Univ.Universe.Set.cardinal levels_to_abstract in
+  let origdepth = depth in
+  let levels_to_abstract, instances_to_abstract = err_if_contains_alg_univ ~depth clause in
+  let db2gr = ref Int.Map.empty in
   let rec subst ~depth m t =
     match E.look ~depth t with
     | E.CData c when isuniv c ->
         begin try E.mkBound (Univ.Universe.Map.find (univout c) m)
         with Not_found -> t end
     | E.App(c,x,xs) ->
+      begin match is_global_or_pglobal ~depth t with
+      | PGlobal(Some gr, Some _) ->
+        let mi = Int.Map.cardinal !db2gr in
+        db2gr := Int.Map.add mi gr !db2gr; in_elpi_pglobal gr (E.mkBound mi)
+      | _ ->
         E.mkApp c (subst ~depth m x) (List.map (subst ~depth m) xs)
+      end
     | E.Cons(x,xs) ->
         E.mkCons (subst ~depth m x) (subst ~depth m xs)
     | E.Lam x ->
@@ -568,21 +590,47 @@ let preprocess_clause ~depth clause =
     | E.UnifVar _ -> CErrors.user_err Pp.(str"The clause begin accumulated contains unification variables, this is forbidden. You must quantify them out using 'pi'.")
     | E.Const _ | E.Nil | E.CData _ -> t
     in
+  let map2hyp map rest =
+    let hyps =
+      Int.Map.bindings map |> List.map @@ fun (i,gr) ->
+        E.mkApp coq_env_globalc gr [in_elpi_pglobal gr (E.mkBound (origdepth+i))] in
+    E.mkAppGlobalL E.Constants.andc (hyps@rest) in
+  let rec add_premises depth t map =
+    match E.look ~depth t with
+    | E.App(c,hd,[pre]) when c == E.Constants.rimplc ->
+      E.mkApp E.Constants.rimplc hd [map2hyp map [pre]]
+    | E.App(c,lam,[]) when c == E.Constants.pic ->
+        begin match E.look ~depth lam with
+        | Lam t -> add_premises (depth+1) t map
+        | _ -> assert false
+        end
+    | _ -> E.mkApp E.Constants.rimplc t [map2hyp map []] in
   let clause = 
-    let rec bind d map = function
+    let rec bind d (map : int Univ.Universe.Map.t) = function
      | [] ->
-         subst ~depth:d map
-           (API.Utils.move ~from:depth ~to_:(depth + levels_to_abstract_no) clause)
+        let clause = API.Utils.move ~from:depth ~to_:d clause in
+        let clause = subst ~depth:d map clause in
+        if Int.Map.is_empty !db2gr then clause
+        else add_premises d clause !db2gr
      | l :: ls ->
        E.mkApp E.Constants.pic (E.mkLam (*   pi x\  *)
            (bind (d+1) (Univ.Universe.Map.add l d map) ls)) []
+     and bindi d (map : int Univ.Universe.Map.t) ua n =
+      if n = 0 then
+         bind d map ua
+      else
+        E.mkApp E.Constants.pic (E.mkLam (*   pi x\  *)
+            (bindi (d+1) map ua (n-1))) []
      in
-       bind depth Univ.Universe.Map.empty
-         (Univ.Universe.Set.elements levels_to_abstract)
+       bindi depth Univ.Universe.Map.empty
+         (Univ.Universe.Set.elements levels_to_abstract) instances_to_abstract
   in
   let vars = collect_term_variables ~depth clause in
+  (* Format.eprintf "CLAUSE=%a\n%!" (Elpi.API.RawPp.term depth) clause; *)
   vars, clause
 
+
+
 let argument_mode = let open Conv in let open API.AlgebraicData in declare {
   ty = TyName "argument_mode";
   doc = "Specify if a predicate argument is in input or output mode";
@@ -883,8 +931,13 @@ let warn_deprecated_add_axiom =
            "section variables is deprecated. Use coq.env.add-axiom or " ^
            "coq.env.add-section-variable instead"))
 
+[%%if coq = "9.2"]
+let comAssumption_declare_variable coe ~kind ty ~univs ~impargs impl ~name =
+  ComAssumption.declare_variable ~coe ~kind ty ~univs ~impargs ~impl ~name:name.CAst.v
+[%%else]
 let comAssumption_declare_variable coe ~kind ty ~univs ~impargs impl ~name =
   ComAssumption.declare_variable ~coe ~kind ty ~univs ~impargs ~impl ~name:name.CAst.v
+[%%endif]
 [%%if coq = "8.20" || coq = "9.0"]
 let comAssumption_declare_axiom coe ~local ~kind ~univs ~impargs ~inline ~name ty =
   ComAssumption.declare_axiom ~coe ~local ~kind ~univs ~impargs ~inline ~name:name.CAst.v ty
@@ -930,32 +983,33 @@ let warns_of_options options = options.user_warns |> Option.map UserWarn.with_em
 let add_axiom_or_variable api id ty local_bkind options state =
   let state, poly, cumul, udecl, _ = poly_cumul_udecl_variance_of_options state options in
   let used = universes_of_term state ty in
+  if not (is_ground (get_sigma state) ty) then
+    err Pp.(str"coq.env.add-const: the type must be ground. Did you forge to call coq.typecheck-indt-decl?");
+  let ty = EConstr.to_constr (get_sigma 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 && Option.has_some local_bkind then
     err Pp.(str api ++ str": section variables cannot be universe polymorphic");
-  let univs = UState.check_univ_decl (Evd.evar_universe_context sigma) udecl ~poly in
+  let univs = UState.check_univ_decl (Evd.evar_universe_context sigma) udecl ~poly ~cumulative:cumul ~kind:UVars.Assumption in
   let kind = Decls.Logical in
   let impargs = [] in
   let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in
   let id = Id.of_string id in
   let name = CAst.(make ~loc id) in
-  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?");
   let gr, _ =
     match local_bkind with
     | Some implicit_kind -> begin
         Dumpglob.dump_definition name true "var";
-        comAssumption_declare_variable Vernacexpr.NoCoercion ~kind (EConstr.to_constr sigma ty) ~univs ~impargs implicit_kind ~name
+        comAssumption_declare_variable Vernacexpr.NoCoercion ~kind ty ~univs ~impargs implicit_kind ~name
       end
     | None -> begin
       Dumpglob.dump_definition name false "ax";
-      comAssumption_declare_axiom Vernacexpr.NoCoercion ~local:Locality.ImportDefaultBehavior ~kind (EConstr.to_constr sigma ty)
+      comAssumption_declare_axiom Vernacexpr.NoCoercion ~local:Locality.ImportDefaultBehavior ~kind ty
         ~univs ~impargs ~inline:options.inline ~name
       end
   in
-  let ucsts = match univs with UState.Monomorphic_entry x, _ -> x | _ -> Univ.ContextSet.empty in
+  let ucsts = match univs.UState.universes_entry_universes with UState.Monomorphic_entry x -> x | _ -> Univ.ContextSet.empty in
   gr, ucsts
   ;;
 
@@ -1281,12 +1335,12 @@ let unify_instances_gref gr ui1 ui2 diag env state cmp_constr_universes =
     | IndRef ind ->
       let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
       let univs = Declareops.inductive_polymorphic_context mib in
-      Conversion.inductive_cumulativity_arguments (mib,snd ind), UVars.AbstractContext.size univs
+      UCompare.inductive_cumulativity_arguments (mib,snd ind), UVars.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
-      Conversion.constructor_cumulativity_arguments (mib,snd ind,kno), UVars.AbstractContext.size univs
+      UCompare.constructor_cumulativity_arguments (mib,snd ind,kno), UVars.AbstractContext.size univs
   in
   let l1 = UVars.Instance.length ui1 in
   let l2 = UVars.Instance.length ui2 in
@@ -1738,7 +1792,8 @@ Supported attributes:
           compute_with_uinstance ~depth options state mk_global gr ui_in in
         let state, t, gls2 =
           closed_ground_term.CConv.embed ~depth ctx csts state t in
-        state, !: maybe_gr +! t, gls @ gls1 @ gls2
+        let maybe_t = match ui_in with Some _ -> None | None -> Some t in
+        state, !: maybe_gr +? maybe_t, gls @ gls1 @ gls2
     | None, None -> err Pp.(str "coq.env.global: no input, all arguments are variables"))),
   DocAbove);
 
@@ -1822,7 +1877,7 @@ Supported attributes:
             UnivGen.fresh_global_instance (get_global_env state) (GlobRef.ConstructRef kon) in
           snd @@ Constr.destConstruct term,
           update_sigma state
-            (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx),
+            (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx),
           []
         else
           UVars.Instance.empty, state, []
@@ -1835,7 +1890,7 @@ Supported attributes:
         let state, lp_uinst, extra_goals = uinstance.Conv.embed ~depth state uinst in
         uinst,
         update_sigma state
-          (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx),
+          (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible sigma ctx),
         API.Conversion.Unify (v', lp_uinst) :: extra_goals
     in
     let ty = if_keep ty (fun () ->
@@ -2132,11 +2187,12 @@ Supported attributes:
 - @using! (default: section variables actually used)
 - @univpoly! (default unset)
 - @udecl! (default unset)
+- @udecl-cumul! (default unset)
 - @dropunivs! (default: false, drops all universe constraints from the store after the definition)
 |})))))),
   (fun id body types opaque _ ~depth {options} _ -> grab_global_env__drop_sigma_univs_if_option_is_set options "coq.env.add-const" (fun state ->
     let local_bkind = if options.local = Some true then Some Glob_term.Explicit else None in
-    let state = minimize_universes state in
+    (* let state = minimize_universes state in *)
     (* Maybe: UState.nf_universes on body and type *)
      match body with
      | B.Unspec -> (* axiom *)
@@ -2151,7 +2207,7 @@ Supported attributes:
     | 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?");
+         err Pp.(str"coq.env.add-const: the body must be ground. Did you forget to call coq.typecheck?");
        let opaque = opaque = B.Given true in
        let types =
          match types, opaque with
@@ -2163,10 +2219,9 @@ Supported attributes:
             | e when CErrors.is_anomaly e -> err Pp.(str"coq.env.add-const: illtyped opaque") end
          | B.Given ty, _ ->
             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?");
+              err Pp.(str"coq.env.add-const: the type must be ground. Did you forge to call coq.typecheck?");
              Some ty 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 Option.has_some local_bkind
         then Locality.Discharge
@@ -2178,7 +2233,7 @@ Supported attributes:
        let hook = Declare.Hook.make (fun { Declare.Hook.S.uctx = x } -> uctx := Some (UState.context_set x)) in
        (* End hack *)
 
-       let info = Declare.Info.make ~scope ~kind ~poly ~udecl ~hook () in
+       let info = Declare.Info.make ~scope ~kind ~poly ~cumulative:cumul ~udecl ~hook () in
 
        let used =
          Univ.Level.Set.union
@@ -2187,7 +2242,12 @@ Supported attributes:
        let used = Univ.Level.Set.union used (universes_of_udecl state udecl) in
        let sigma = restricted_sigma_of used state in
    
-       let gr, uctx = declare_definition uctx options.using ~cinfo ~info ~opaque ~body sigma in
+       let gr, uctx =
+         try declare_definition uctx options.using ~cinfo ~info ~opaque ~body sigma
+       with Loop_checking.Undeclared l as e ->
+          Printf.eprintf "Loop_checking.Undeclared %s\n%!" (Univ.Level.to_string l);
+          raise e
+        in
        let () =
         let lid = CAst.make ~loc:(to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state) (Id.of_string id) in
         match scope with
@@ -2256,8 +2316,8 @@ Supported attributes:
        match me.mind_entry_universes with
        | Monomorphic_ind_entry -> (Monomorphic_entry, UState.Monomorphic_entry uctx, univ_binders)
        | Template_ind_entry _ -> nYI "template polymorphic inductives"
-       | Polymorphic_ind_entry uctx ->
-          (Polymorphic_entry uctx, UState.Polymorphic_entry uctx, univ_binders)
+       | Polymorphic_ind_entry (uctx, variances) ->
+          (Polymorphic_entry (uctx, variances), UState.Polymorphic_entry (uctx, variances), univ_binders)
        in
      let () = global_push_context_set uctx in
      let mind =
@@ -2566,16 +2626,17 @@ phase unnecessary.|};
     | Data u1, Data u2 ->
         if Sorts.equal u1 u2 then Univ.ContextSet.empty, state, !: u1 +! u2,[]
         else
-          let state, u2 = if true (* options.algunivs != Some true *)
+          let state, u2 = if options.algunivs != Some true
           then purge_algebraic_univs_sort state (EConstr.ESorts.make u2)
           else state, u2 in
         Univ.ContextSet.empty, add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[]
-    | _ -> err Pp.(str"coq.sort.leq: called with _ as argument")))),
+    | _ ->
+      err Pp.(str"coq.sort.leq: called with _ as argument")))),
   DocAbove);
 
   MLCode(Pred("coq.sort.eq",
-    CInOut(B.ioargC_flex sort, "S1",
-    CInOut(B.ioargC_flex sort, "S2",
+    CInOut(B.ioargC_flex sort, "S1", (* FIXME (not out) *)
+    CInOut(B.ioargC_flex sort, "S2", (* FIXME (not out) *)
     Full(global, "constrains S1 = S2"))),
   (fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.eq"
   (fun state ->
@@ -2583,7 +2644,7 @@ phase unnecessary.|};
     | Data u1, Data u2 ->
       if Sorts.equal u1 u2 then Univ.ContextSet.empty, state, !: u1 +! u2,[]
       else
-        let state, u2 = if true (* options.algunivs != Some true *)
+        let state, u2 = if options.algunivs != Some true
         then purge_algebraic_univs_sort state (EConstr.ESorts.make u2)
         else state, u2 in
         Univ.ContextSet.empty, add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, []
@@ -2596,20 +2657,18 @@ phase unnecessary.|};
     Full(global,  "constrains S2 = S1 + 1"))),
   (fun u1 u2 ~depth _ _ state ->
     match u1, u2 with
-    | Data u1, Data u2 -> univ_super state u1 u2, !: u1 +! u2, []
+    | Data u1, Data u2 -> univ_super state u1 u2, !: u1 +! u2, [] (* FIXME  *)
     | _ -> err Pp.(str"coq.sort.sup: called with _ as argument"))),
   DocAbove);
 
   MLCode(Pred("coq.sort.pts-triple",
-    CInOut(B.ioargC_flex sort, "S1",
-    CInOut(B.ioargC_flex sort, "S2",
+    CIn(sort, "S1",
+    CIn(sort, "S2",
     COut(sort, "S3",
     Full(global,  "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);
+    let state, u3 = univ_product state u1 u2 in state, !: u3, [])),
+  DocAbove);
 
   MLCode(Pred("coq.univ.print",
     Read(unit_ctx,  "prints the set of universe constraints"),
@@ -2719,7 +2778,8 @@ phase unnecessary.|};
       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
+      let v = Univ.Universe.make v in
+      let v_constraints = Univ.Constraints.filter (fun (l1,_,l2) -> Univ.Universe.(equal v l1 || equal v l2)) constraints in
       state, !: (Univ.Constraints.elements v_constraints), []
     )),
   DocAbove);
@@ -2736,11 +2796,9 @@ phase unnecessary.|};
  
   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.
+  LPDoc {|A universe polymorphic constant can be instantiated with universes.
 
-A univ-instance is morally a list of universe level variables,
+A univ-instance is morally a list of universes,
 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.
 
@@ -2757,20 +2815,22 @@ term (of the instance it contains) with another one.|};
   (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
+      let elpi_term_of_univ state u =
+        let state, t, gls = univ.Conv.embed ~depth state u in
         assert (gls = []);
         state, mkData t
       in
       let quals, univs = UVars.Instance.to_array uinst in
       let () = if not (CArray.is_empty quals) then nYI "sort poly" in
       let state, univs =
-        CArray.fold_left_map elpi_term_of_level state univs in
+        CArray.fold_left_map elpi_term_of_univ state univs 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
+        | NoData -> let state, (_,u) = new_univ_level_variable state in state, u, []
+        | Data t -> let state, l, gls = universe_level_variable.Conv.readback ~depth state t in
+        state, Univ.Universe.make l, gls
+      in
       let state, levels, gls = U.map_acc readback_or_new state univs in
       state, !: (UVars.Instance.of_array ([||], Array.of_list levels)) +? None, gls
     | NoData, NoData ->
diff --git a/src/rocq_elpi_glob_quotation.ml b/src/rocq_elpi_glob_quotation.ml
index 6a275cde5..c0254a88f 100644
--- a/src/rocq_elpi_glob_quotation.ml
+++ b/src/rocq_elpi_glob_quotation.ml
@@ -216,7 +216,27 @@ let universe_level_name evd ({CAst.v=id} as lid) =
     CErrors.user_err ?loc:lid.CAst.loc
       (Pp.(str "Undeclared universe: " ++ Id.print id ++ str "."))
 
-let sort_name env sigma l = match l with
+let glob_level loc state = function
+    | GSProp 
+    | GProp ->
+      CErrors.user_err ?loc
+        Pp.(str "Universe instances cannot contain non-Set small levels, polymorphic" ++
+            str " universe instances must be greater or equal to Set.");
+    | GSet -> Univ.Level.set
+    | GUniv u -> u
+    | GRawUniv u -> nYI "GRawUniv"
+    | GLocalUniv l -> universe_level_name (get_sigma state) l
+
+let glob_level_expr loc state (l, k) =
+  (glob_level loc state l, k)
+
+let glob_univ loc state = function
+  | UAnonymous _ -> nYI "UAnonymous"
+  | UNamed l ->
+    let us = List.map (glob_level_expr loc state) l in
+    Univ.Universe.of_list us
+
+let sort_name loc state l = match l with
 | [] -> assert false
 | [u, 0] ->
   begin match u with
@@ -225,30 +245,18 @@ let sort_name env sigma l = match l with
   | GProp -> Sorts.prop
   | GUniv u -> Sorts.sort_of_univ (Univ.Universe.make u)
   | GLocalUniv l ->
-    let u = universe_level_name sigma l in
+    let u = universe_level_name (get_sigma state) l in
     Sorts.sort_of_univ (Univ.Universe.make u)
   | GRawUniv _ -> nYI "GRawUniv"
   end
-| [_] | _ :: _ :: _ ->
-  nYI "(glob)HOAS for Type@{i j}"
+  | l -> 
+    let us = List.map (glob_level_expr loc state) l in
+    Sorts.sort_of_univ (Univ.Universe.of_list us)
 
-let glob_level loc state = function
-  | UAnonymous _ -> nYI "UAnonymous"
-  | UNamed s ->
-      match s with
-      | GSProp 
-      | GProp ->
-        CErrors.user_err ?loc
-          Pp.(str "Universe instances cannot contain non-Set small levels, polymorphic" ++
-              str " universe instances must be greater or equal to Set.");
-      | GSet -> Univ.Level.set
-      | GUniv u -> u
-      | GRawUniv u -> nYI "GRawUniv"
-      | GLocalUniv l -> universe_level_name (get_sigma state) l
 
 let nogls f ~depth state = let state, x = f ~depth state in state, x, ()
 
-let rigid_anon_type = function GSort(None, UAnonymous {rigid=UnivRigid}) -> true | _ -> false
+let rigid_anon_type = function GSort(None, UAnonymous {rigid=_}) -> true | _ -> false
 let named_type = function GSort(None, UNamed _) -> true | _ -> false
 let name_of_type = function GSort(None, UNamed u) -> u | _ -> assert false
 let dest_GProd = function GProd(n,_,_,s,t) -> n,s,t | _ -> assert false
@@ -344,7 +352,7 @@ let gterm2lpast ~pattern ~language state glob =
       in_elpiast_poly_gr ~loc gr s
     | Some (ql,l) ->
       let () = if not (CList.is_empty ql) then nYI "sort poly" in
-      let l' = List.map (glob_level x.CAst.loc state) l in
+      let l' = List.map (glob_univ x.CAst.loc state) l in
       in_elpiast_poly_gr_instance ~loc gr (UVars.Instance.of_array ([||], Array.of_list l'))
     end
   | GRef(gr,_ul) -> in_elpiast_gr ~loc gr
@@ -355,7 +363,7 @@ let gterm2lpast ~pattern ~language state glob =
   | GSort _ as t when named_type t ->
       let u = name_of_type t in
       let env = get_glob_env state in
-      in_elpiast_sort ~loc state (sort_name env (get_sigma state) u)
+      in_elpiast_sort ~loc state (sort_name x.CAst.loc state u)
   | GSort(_) -> nYI "(glob)HOAS for Type@{i j}"
 
   | GProd _ as t ->
diff --git a/src/rocq_elpi_programs.ml b/src/rocq_elpi_programs.ml
index 3fd6a4169..40f581e58 100644
--- a/src/rocq_elpi_programs.ml
+++ b/src/rocq_elpi_programs.ml
@@ -973,8 +973,8 @@ let file_resolver ?cwd:_ ~unit:file () =
 let versions =
   let open API.Setup.StrMap in
   empty
-  |> add "coq-elpi" (API.Utils.version_parser ~what:"coq-elpi" "%%VERSION_NUM%%")
-  |> add "rocq-elpi" (API.Utils.version_parser ~what:"rocq-elpi" "%%VERSION_NUM%%")
+  |> add "coq-elpi" (API.Utils.version_parser ~what:"coq-elpi" "2.5.2-45-gca1b82d")
+  |> add "rocq-elpi" (API.Utils.version_parser ~what:"rocq-elpi" "2.5.2-45-gca1b82d")
   |> add "coq" (API.Utils.version_parser ~what:"coq" Coq_config.version)
   |> add "rocq" (API.Utils.version_parser ~what:"rocq" Coq_config.version)
           
diff --git a/src/rocq_elpi_utils.ml b/src/rocq_elpi_utils.ml
index 6ce1e8ae0..9cb05f4a7 100644
--- a/src/rocq_elpi_utils.ml
+++ b/src/rocq_elpi_utils.ml
@@ -358,7 +358,9 @@ let detype_sort ku sigma x =
   | Set -> glob_Set_sort
   | Type u when ku -> None, detype_universe sigma u
   | QSort (q, u) when ku -> Some (detype_qvar sigma q), detype_universe sigma u
-  | _ -> glob_Type_sort
+  | _ -> 
+    let glob_Type_sort = None, Glob_term.UAnonymous {rigid=UnivFlexible} in (* Fixed version from Glob_ops *)
+    glob_Type_sort
 
 (*
 let detype_relevance_info sigma na =
@@ -377,7 +379,7 @@ let detype_instance ku sigma l =
     else
       let qs, us = UVars.Instance.to_array l in
       let qs = List.map (detype_quality sigma) (Array.to_list qs) in
-      let us = List.map (detype_level sigma) (Array.to_list us) in
+      let us = List.map (detype_universe sigma) (Array.to_list us) in
       Some (qs, us)
 
 let it_destRLambda_or_LetIn_names l c =
diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v
index 12b7a01bf..e724a1b50 100644
--- a/tests/test_HOAS.v
+++ b/tests/test_HOAS.v
@@ -66,19 +66,28 @@ Elpi Query lp:{{
   coq.env.end-section
 }}.
 
-Elpi Db univs.db lp:{{ pred u o:univ. }}.
+Polymorphic Definition ut@{u} : Type@{u} := Type.
+
+Elpi Db univs.db lp:{{
+   pred u o:univ.
+   pred ut o:term, o:univ.
+  }}.
 Elpi Command test_u.
 Elpi Accumulate Db univs.db.
 Elpi Query lp:{{
   coq.univ.new U,
-  coq.elpi.accumulate current "univs.db" (clause _ _ (u U))
+  coq.elpi.accumulate current "univs.db" (clause _ _ (u U)),
+  coq.univ.variable U L,
+  coq.univ-instance I [L],
+  coq.elpi.accumulate current "univs.db" (clause _ _ (ut (pglobal {{:gref ut}} I) U))
 }}.
 
 Universe foo.
-
+Universe foo1.
+Elpi Print test_u "elpi.tests/test_u".
 Elpi Query lp:{{
   {{ Type@{foo} }} = sort (typ U),
-  coq.elpi.accumulate current "univs.db" (clause _ _ (u U))
+  u U, ut {{ ut@{foo} }} U
 }}.
 
 
diff --git a/tests/test_polymorphism.v b/tests/test_polymorphism.v
new file mode 100644
index 000000000..9a46ff1ff
--- /dev/null
+++ b/tests/test_polymorphism.v
@@ -0,0 +1,68 @@
+From elpi Require Import elpi.
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+Set Printing Universes.
+
+Module test_rocq.
+Record test : Type := mktest { foo : Type }.
+Print test. (* Record test@{u} : Type@{u+1} := mktest { foo : Type@{u} }. (* u |=  *)*)
+End test_rocq.
+Module test_elpi.
+Elpi Command test_default.
+Elpi Query lp:"
+   coq.env.add-indt (record ""test"" {{Type}} ""mktest""
+     (field _ ""foo"" {{Type}}  _ \ end-record)) _C.
+".
+Print test. (* Record test : Type@{test.u0} := mktest { foo : Type@{test.u1} }. *)
+(* we get a monomorphic universe *)
+End test_elpi.
+
+Module test_explicit.
+Elpi Command test_explicit.
+Elpi Query lp:"
+   @keep-alg-univs! => @univpoly-cumul! => coq.env.add-indt (record ""test"" {{Type}} ""mktest""
+     (field _ ""foo"" {{Type}}  _ \ end-record)) _C.
+".
+Print test.
+(* Record test@{u} : Type@{u+1} := mktest { foo : Type@{u} }. *)
+(* u(+ (= for typing) in term, + in type) |= *)
+(* It's indeed polymorphic and we do get the minimized version *)
+End test_explicit.
+
+Module test_explicit2.
+Elpi Command test_explicit2.
+Elpi Query lp:"
+  coq.univ.new U,
+   @keep-alg-univs! => @univpoly-cumul! =>
+    coq.env.add-indt (record ""test"" (sort (typ U+1)) ""mktest""
+     (field _ ""foo"" (sort (typ U))  _ \ end-record)) _C.
+".
+Print test.
+(* Record test@{u} : Type@{u+1} := mktest { foo : Type@{u} }. *)
+(* u(+ (= for typing) in term, + in type) |= *)
+(* It's indeed polymorphic and we do get the minimized version *)
+End test_explicit2.
+
+Module test_minimization.
+Elpi Command test_minimization.
+Elpi Query lp:"
+   coq.univ.new U,
+   coq.univ.variable U V,
+   @keep-alg-univs! => @udecl-cumul! [(auto V)] ff [] tt => coq.env.add-indt (record ""test"" (sort (typ _)) ""mktest""
+     (field _ ""foo"" (sort (typ U))  _ \ end-record)) _C.
+".
+Print test.
+(* It's indeed polymorphic and we do get the minimized version *)
+End test_minimization.
+
+Module test_cumul_def.
+Elpi Command test_cumul_def.
+
+Elpi Query lp:"
+   coq.univ.new U,
+   coq.univ.variable U V,
+   @keep-alg-univs! => @udecl-cumul! [(auto V)] tt [] tt => coq.env.add-const ""polydef"" (sort (typ U)) _ _ _C.
+".
+  Print polydef.
+Print test_cumul_def.
+End test_cumul_def.