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.
---
 theories/Init/Tactics.v | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'theories')

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