[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, 2 insertions, 5 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 73b523f0b3..bf4567e57f 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -74,13 +74,10 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  let evd, ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in
-  let uctx = Evd.evar_universe_context evd in
-  let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+  let ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in
   let kind = Decls.IsDefinition kind in
-  let ubind = Evd.universe_binders evd in
   let _ : Names.GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce
+    DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs ce
   in ()
 
 let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =