From ec23372744683b8d0b5dfa01eb731c33e73fef4e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 30 Jun 2020 14:26:59 +0200
Subject: [declare] Return both declared constants in Derive path.

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

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 28e6f21d41..52be6f7946 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -2014,7 +2014,7 @@ let finish_derived ~f ~name ~entries =
   let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in
   let lemma_def = DefinitionEntry lemma_def in
   let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
-  [GlobRef.ConstRef ct]
+  [GlobRef.ConstRef f_kn; GlobRef.ConstRef ct]
 
 let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 =
 
-- 
cgit v1.2.3