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/comAssumption.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index f9b73a59eb..a0b0dcf4c8 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -217,7 +217,7 @@ let context_insection sigma ~poly ctx =
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
         let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
-            ~kind:Decls.Definition UnivNames.empty_binders entry []
+            ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry []
         in
         ()
     in
-- 
cgit v1.2.3