Support cumulative definitions

Author: mattam82

src/rocq_elpi_builtins.ml

@@ -2145,6 +2145,7 @@ 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 ->
@@ -2191,7 +2192,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

tests/test_polymorphism.v

@@ -29,12 +29,26 @@ Print test.
 (* 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! [V] ff [] tt => coq.env.add-indt (record ""test"" (sort (typ _)) ""mktest""
+   @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.