From 11fb93285b2e7c528d8abe7da5924d84e0a97002 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 25 Oct 2019 00:30:07 +0200
Subject: [declare] Generalize kind type on declareDef

This is useful to remove some duplicate bits in other declare files.
---
 vernac/declareDef.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 54a0c9a7e8..d6001f5970 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -42,7 +42,7 @@ end
 val declare_definition
   :  name:Id.t
   -> scope:locality
-  -> kind:Decls.definition_object_kind
+  -> kind:Decls.logical_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> UnivNames.universe_binders
   -> Evd.side_effects Declare.proof_entry
-- 
cgit v1.2.3