diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-05 16:59:33 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-05 16:59:33 +0200 |
| commit | 0e6e585c1234e0d67b3c703a548c366f443d71d0 (patch) | |
| tree | 8dfbf2c364018d006646370194d869356b0a73b1 /theories | |
| parent | 7001fd206db7f4a22d473b5f5a7c7fd6d28039e4 (diff) | |
| parent | ca4aee0fcf1b54363a6a1eb837cd05cd7ffcc0d9 (diff) | |
Merge PR#605: Report a useful error for dependent induction
Diffstat (limited to 'theories')
| -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 5d1e87ae0..7a846cd1b 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.]". |