From ca4aee0fcf1b54363a6a1eb837cd05cd7ffcc0d9 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Wed, 3 May 2017 07:47:51 -0400
Subject: 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].
---
 theories/Init/Tactics.v | 7 +++++++
 1 file changed, 7 insertions(+)

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.]".
-- 
cgit v1.2.3