Universes clauses

.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";
 
 }

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.

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"

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))

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.
 

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"