From a6d663c85d71b3cce007af23419e8030b8c5ac88 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:57:44 +0200
Subject: [declare] [api] Removal of duplicated type aliases.

---
 vernac/comHints.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comHints.ml')

diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index ec37ec7fa8..b05bf9a675 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -56,7 +56,7 @@ let project_hint ~poly pri l2r r =
     Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c))
   in
   let c =
-    Declare.declare_constant ~local:Declare.ImportDefaultBehavior ~name
+    Declare.declare_constant ~local:Locality.ImportDefaultBehavior ~name
       ~kind:Decls.(IsDefinition Definition)
       cb
   in
-- 
cgit v1.2.3