diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 7fbad3ea96..68ae5628db 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -8,5 +8,5 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - edeclare ~name ~poly ~scope:Decl_kinds.(Global ImportDefaultBehavior) + edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None [] |