diff options
| author | Tej Chajed | 2017-05-03 07:47:51 -0400 |
|---|---|---|
| committer | Tej Chajed | 2017-05-03 07:53:04 -0400 |
| commit | ca4aee0fcf1b54363a6a1eb837cd05cd7ffcc0d9 (patch) | |
| tree | 823ddd0a7da01cfe86be3edd8181b64dbd5c43fb /dev | |
| parent | 3c795ba6b5728e8a0a699ab15c773c52c48f33e4 (diff) | |
Report a useful error for dependent induction
The dependent induction tactic notation is in the standard library but
not loaded by default, leading to a parser error message that is
confusing and unhelpful. This commit adds a notation for dependent
induction to Init that fails and reports [Require Import
Coq.Program.Equality.] is required to use [dependent induction].
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions