diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index 432921064..19df2ce79 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -957,6 +957,9 @@ external pred coq.univ.print .
 % [coq.univ.new U] A fresh universe.
 external pred coq.univ.new o:univ.
 
+% [coq.univ.super U U1] relates a univ U to its successor U1
+external pred coq.univ.super i:univ, o:univ.
+
 % [coq.univ Name U] Finds a named unvierse. Can fail.
 external pred coq.univ o:id, o:univ.
 
diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index baa659091..de76883d9 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -913,9 +913,9 @@ let purge_algebraic_univs_sort state s =
 
 let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []
 
-let sort = { sort with API.Conversion.embed = (fun ~depth state s ->
+(* 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) }
+  sort.API.Conversion.embed ~depth state s) } *)
 
 let in_elpi_sort ~depth state s =
   let state, s, gl = sort.API.Conversion.embed ~depth state s in
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 5fb0ce1f3..5952b8ceb 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -2311,7 +2311,7 @@ phase unnecessary.|};
     | Data u1, Data u2 ->
         if Sorts.equal u1 u2 then state, !: u1 +! u2,[]
         else
-          let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in
+          (* let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in *)
           add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[]
     | _ -> err Pp.(str"coq.sort.leq: called with _ as argument"))),
   DocAbove);
@@ -2325,7 +2325,7 @@ phase unnecessary.|};
     | Data u1, Data u2 ->
       if Sorts.equal u1 u2 then state, !: u1 +! u2,[]
       else
-        let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in
+        (* let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in *)
         add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, []
     | _ -> err Pp.(str"coq.sort.eq: called with _ as argument"))),
   DocAbove);
@@ -2369,6 +2369,23 @@ phase unnecessary.|};
      state, !: u, [])),
   DocAbove);
 
+  MLCode(Pred("coq.univ.super",
+    In(univ,"U",
+    Out(univ,"U1",
+    Full(unit_ctx,  "relates a univ U to its successor U1"))),
+  (fun u _ ~depth _ _ state ->
+    state, !: (Univ.Universe.super u), [])),
+  DocAbove);
+
+  MLCode(Pred("coq.univ.max",
+    In(univ,"U1",
+    In(univ,"U2",
+    Out(univ,"UMax",
+    Full(unit_ctx,  "relates univs U1 and U2 to their max UMax")))),
+  (fun u1 u2 _ ~depth _ _ state ->
+    state, !: (Univ.Universe.sup u1 u2), [])),
+  DocAbove);
+
   MLCode(Pred("coq.univ",
     InOut(B.ioarg id, "Name",
     InOut(B.ioarg univ, "U",