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/4663.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/4663.v')
| -rw-r--r-- | test-suite/bugs/closed/4663.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4663.v b/test-suite/bugs/closed/4663.v new file mode 100644 index 000000000..b76619882 --- /dev/null +++ b/test-suite/bugs/closed/4663.v @@ -0,0 +1,3 @@ +Coercion foo (n : nat) : Set. +Admitted. +Check (0 : Set). |