done by coq

src/coq_elpi_builtins.ml

@@ -942,19 +942,18 @@ let pattern_of_glob_constr env g = Patternops.pattern_of_glob_constr env g
 [%%endif]
 
 [%%if coq = "8.19"]
-let declare_definition ~poly hack _using ~cinfo ~info ~opaque ~body sigma =
+let declare_definition hack _using ~cinfo ~info ~opaque ~body sigma =
   let gr = Declare.declare_definition ~cinfo ~info ~opaque ~body sigma in
   gr, Option.get !hack
 [%%elif coq = "8.20"]
-let declare_definition ~poly hack using ~cinfo ~info ~opaque ~body sigma =
+let declare_definition hack using ~cinfo ~info ~opaque ~body sigma =
   let using = Option.map Proof_using.using_from_string using in
   let gr = Declare.declare_definition ~cinfo ~info ~opaque ~body ?using sigma in
   gr, Option.get !hack
 [%%else]
-let declare_definition ~poly _ using ~cinfo ~info ~opaque ~body sigma =
+let declare_definition _ using ~cinfo ~info ~opaque ~body sigma =
   let using = Option.map Proof_using.using_from_string using in
-  let gr, uctx = Declare.declare_definition_full ~cinfo ~info ~opaque ~body ?using sigma in
-  gr, if poly then Univ.ContextSet.empty else uctx
+  Declare.declare_definition_full ~cinfo ~info ~opaque ~body ?using sigma
 [%%endif]
 
 
@@ -2078,7 +2077,7 @@ Supported attributes:
        let used = Univ.Level.Set.union used (universes_of_udecl state udecl) in
        let sigma = restricted_sigma_of used state in
    
-       let gr, uctx = declare_definition ~poly uctx options.using ~cinfo ~info ~opaque ~body sigma in
+       let gr, uctx = declare_definition uctx options.using ~cinfo ~info ~opaque ~body sigma in
        let () =
         let lid = CAst.make ~loc:(to_coq_loc @@ State.get Coq_elpi_builtins_synterp.invocation_site_loc state) (Id.of_string id) in
         match scope with