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 | |
| 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].
| -rw-r--r-- | theories/Init/Tactics.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 5d1e87ae0c..7a846cd1b3 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -236,3 +236,10 @@ Tactic Notation "clear" "dependent" hyp(h) := Tactic Notation "revert" "dependent" hyp(h) := generalize dependent h. + +(** Provide an error message for dependent induction that reports an import is +required to use it. Importing Coq.Program.Equality will shadow this notation +with the actual [dependent induction] tactic. *) + +Tactic Notation "dependent" "induction" ident(H) := + fail "To use dependent induction, first [Require Import Coq.Program.Equality.]". |