diff options
| author | Maxime Dénès | 2017-05-05 16:59:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-05 16:59:33 +0200 |
| commit | 0e6e585c1234e0d67b3c703a548c366f443d71d0 (patch) | |
| tree | 8dfbf2c364018d006646370194d869356b0a73b1 /dev | |
| parent | 7001fd206db7f4a22d473b5f5a7c7fd6d28039e4 (diff) | |
| parent | ca4aee0fcf1b54363a6a1eb837cd05cd7ffcc0d9 (diff) | |
Merge PR#605: Report a useful error for dependent induction
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions