diff options
| author | Gaëtan Gilbert | 2019-01-25 16:41:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-25 22:46:09 +0100 |
| commit | 0a0d551646ffa105104e418ba7e4274d52cbf8ac (patch) | |
| tree | 9c31b80a64b2ec941b7d37e40076ac153cb5f57e /plugins/syntax | |
| parent | 6994539744e4ffaa4f622c8bccc66276e445ae9a (diff) | |
Move non-primitive-record warning to declare_mutual_inductive_with_eliminations
This makes it print the warning before the definition message, so if
we run with +non-primitive-record we don't see
"""
defined foo
error could not define foo
"""
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions