[declareDef] More consistent handling of universe binders

The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook

We handle this automatically now; it seems like a reasonably good API
improvement.

However, it is not clear what we do now is right for all cases; must
check.

1 files changed, 3 insertions, 2 deletions

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index cb9acda770..4a82696ea6 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -204,9 +204,10 @@ let context_insection sigma ~poly ctx =
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
         (* XXX Fixme: Use DeclareDef.prepare_definition *)
-        let entry = DeclareDef.ClosedDef.of_proof_entry entry in
+        let uctx = Evd.evar_universe_context sigma in
+        let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in
         let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
-            ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry
+            ~kind:Decls.(IsDefinition Definition) ~impargs:[] entry
         in
         ()
     in