From cc06679015013fa26736e10227967cd38be3d6b5 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 15 Oct 2020 09:17:15 -0500
Subject: Report a useful error for dependent destruction

Similar to `dependent induction`, report an error message for `dependent
destruction` saying that importing `Coq.Program.Equality` is required,
rather than failing at parsing time.

This is a small extension of #605 to cover dependent destruction as
well. Here I also put in some tests.
---
 test-suite/output/DependentInductionErrors.out |  4 ++++
 test-suite/output/DependentInductionErrors.v   | 17 +++++++++++++++++
 theories/Init/Tactics.v                        |  9 ++++++---
 3 files changed, 27 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/output/DependentInductionErrors.out
 create mode 100644 test-suite/output/DependentInductionErrors.v

diff --git a/test-suite/output/DependentInductionErrors.out b/test-suite/output/DependentInductionErrors.out
new file mode 100644
index 0000000000..4a83375f6f
--- /dev/null
+++ b/test-suite/output/DependentInductionErrors.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+Tactic failure: To use dependent destruction, first [Require Import Coq.Program.Equality.].
+The command has indeed failed with message:
+Tactic failure: To use dependent induction, first [Require Import Coq.Program.Equality.].
diff --git a/test-suite/output/DependentInductionErrors.v b/test-suite/output/DependentInductionErrors.v
new file mode 100644
index 0000000000..2fce00f9fd
--- /dev/null
+++ b/test-suite/output/DependentInductionErrors.v
@@ -0,0 +1,17 @@
+Theorem foo (b:bool) : b = true \/ b = false.
+Proof.
+  Fail dependent destruction b.
+  Fail dependent induction b.
+Abort.
+
+From Coq Require Import Program.Equality.
+
+Theorem foo_with_destruction (b:bool) : b = true \/ b = false.
+Proof.
+  dependent destruction b; auto.
+Qed.
+
+Theorem foo_with_induction (b:bool) : b = true \/ b = false.
+Proof.
+  dependent induction b; auto.
+Qed.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index e1db68aea9..35bab1021e 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -245,13 +245,16 @@ 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. *)
+(** Provide an error message for dependent induction/dependent destruction that
+    reports an import is required to use it. Importing Coq.Program.Equality will
+    shadow this notation with the actual tactics. *)
 
 Tactic Notation "dependent" "induction" ident(H) :=
   fail "To use dependent induction, first [Require Import Coq.Program.Equality.]".
 
+Tactic Notation "dependent" "destruction" ident(H) :=
+  fail "To use dependent destruction, first [Require Import Coq.Program.Equality.]".
+
 (** *** [inversion_sigma] *)
 (** The built-in [inversion] will frequently leave equalities of
     dependent pairs.  When the first type in the pair is an hProp or
-- 
cgit v1.2.3