Add a test for change over case nodes.

This is extracted from #13563.

1 files changed, 20 insertions, 0 deletions

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.