From b2aae7ba35a90e695d34f904c74f5156385344a9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 13:21:48 +0200
Subject: [api] Move `locality` from `library` to `vernac`.

This datatype does belong to this layer.
---
 doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/plugin_tutorial')

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 []
-- 
cgit v1.2.3