✨ Add coq.univ.super

Author: ecranceMERCE

coq-builtin.elpi

@@ -974,6 +974,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.
 

src/coq_elpi_builtins.ml

@@ -2344,6 +2344,14 @@ 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",
     InOut(B.ioarg id, "Name",
     InOut(B.ioarg univ, "U",