1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index e82fb3e3b1..d74fdcab2c 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -13,12 +13,14 @@ open Declare
 open Globnames
 open Impargs
 
+type locality = Discharge | Global of Declare.import_status
+
 (* Hooks naturally belong here as they apply to both definitions and lemmas *)
 module Hook = struct
   module S = struct
     type t = UState.t
       -> (Names.Id.t * Constr.t) list
-      -> Decl_kinds.locality
+      -> locality
       -> Names.GlobRef.t
       -> unit
   end