aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-05-03 11:02:05 +0200
committerGuillaume Melquiond2016-05-03 11:02:05 +0200
commitf51dca0647b3213eb20a9b004372e5e6182bb29a (patch)
treebb680e0dd8ac28fe9b3f3b4b190df9459403ee9d /kernel
parent24a125b779c0cf6e9b0662e122c74aa80eb1837b (diff)
Call hooks when terminating a definition proof (bug #4663).
Also register properly the kind of definition.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions