[comDefinition] Use prepare function from DeclareDef.

We also update the plugin tutorial.

This was already tried [in the same exact way] in #8811, however the
bench time was not convincing then, but now things seem a bit better,
likely due to the removal of some extra normalization somewhere.

Some more changes from #8811 are still pending.

1 files changed, 2 insertions, 11 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 23f8fbe888..3c0355c92d 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,17 +1,8 @@
-(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
 let edeclare ?hook ~ontop ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
-  let sigma = Evd.minimize_universes sigma in
-  let body = EConstr.to_constr sigma body in
-  let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
-  let uvars_fold uvars c =
-    Univ.LSet.union uvars (Vars.universes_of_constr c) in
-  let uvars = List.fold_left uvars_fold Univ.LSet.empty
-     (Option.List.cons tyopt [body]) in
-  let sigma = Evd.restrict_universe_context sigma uvars in
-  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
+      ~opaque ~poly sigma udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
   let ubinders = Evd.universe_binders sigma in
-  let ce = Declare.definition_entry ?types:tyopt ~univs body in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
   DeclareDef.declare_definition ~ontop ident k ce ubinders imps ?hook_data