Add test for pi_eq_proofs.

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/success/programequality.v b/test-suite/success/programequality.v
new file mode 100644
index 0000000000..414c572f81
--- /dev/null
+++ b/test-suite/success/programequality.v
@@ -0,0 +1,13 @@
+Require Import Program.
+
+Axiom t : nat -> Set.
+
+Goal forall (x y : nat) (e : x = y) (e' : x = y) (P : t y -> x = y -> Type)
+       (a : t x),
+    P (eq_rect _ _ a _ e) e'.
+Proof.
+  intros.
+  pi_eq_proofs. clear e.
+  destruct e'. simpl.
+  change (P a eq_refl).
+Abort.
\ No newline at end of file