diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 13 |
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 |