From 2ecba80ce61efe7572a99ade8a5b6a39ea33d1a7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 17 Dec 2020 11:03:01 +0100
Subject: Add a test for change over case nodes.

This is extracted from #13563.
---
 test-suite/success/change_case.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 test-suite/success/change_case.v

diff --git a/test-suite/success/change_case.v b/test-suite/success/change_case.v
new file mode 100644
index 0000000000..490e4f4b6c
--- /dev/null
+++ b/test-suite/success/change_case.v
@@ -0,0 +1,20 @@
+Inductive box (A : Type) := Box : A -> box A.
+
+Axiom PRED : unit -> Prop.
+Axiom FUN : forall (u : unit), box (PRED u).
+
+Axiom U : unit.
+Definition V := U.
+
+Goal match FUN U with Box _ _ => True end.
+Proof.
+repeat match goal with
+| [ |- context G[ U ] ] =>
+ let e := context G [ V ] in
+ change e
+end.
+set (Z := V).
+clearbody Z. (* This fails if change misses the case parameters *)
+destruct (FUN Z).
+constructor.
+Qed.
-- 
cgit v1.2.3