diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-03 11:02:05 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-03 11:02:05 +0200 |
| commit | f51dca0647b3213eb20a9b004372e5e6182bb29a (patch) | |
| tree | bb680e0dd8ac28fe9b3f3b4b190df9459403ee9d /test-suite/bugs/closed/4203.v | |
| parent | 24a125b779c0cf6e9b0662e122c74aa80eb1837b (diff) | |
Call hooks when terminating a definition proof (bug #4663).
Also register properly the kind of definition.
Diffstat (limited to 'test-suite/bugs/closed/4203.v')
0 files changed, 0 insertions, 0 deletions