diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index eb8161c2bb..7fbad3ea96 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,14 +1,12 @@ -let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = +let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps = 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 hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ident k ce ubinders imps ?hook_data + DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data -let declare_definition ~poly ident sigma body = - let k = Decl_kinds.(Global ImportDefaultBehavior, poly, Definition) in +let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - edeclare ident k ~opaque:false sigma udecl body None [] - -(* But this definition cannot be undone by Reset ident *) + edeclare ~name ~poly ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None [] |