diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 14:26:59 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-08-31 21:08:29 +0200 |
| commit | ec23372744683b8d0b5dfa01eb731c33e73fef4e (patch) | |
| tree | b0b2bb6859ae8cdfc820a5b349869ec5c04d0ef5 /vernac | |
| parent | 84a32bbdf6572a45a78667803e574a561bbed21f (diff) | |
[declare] Return both declared constants in Derive path.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 = |