From 4c0c4b46993aeb31786d60cb278cfb317dea454e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 8 Jul 2016 11:49:06 +0200
Subject: Add test for pi_eq_proofs.

---
 test-suite/success/programequality.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/success/programequality.v

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
-- 
cgit v1.2.3