Also support cumulative definitions and add a test for them.

Author: mattam82

src/rocq_elpi_builtins.ml

@@ -2180,7 +2180,6 @@ Supported attributes:
               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 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

tests/test_polymorphism.v

@@ -53,4 +53,15 @@ Elpi Query lp:"
 ".
 Print test.
 (* It's indeed polymorphic and we do get the minimized version *)
-End test_minimization.
+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.