From 90c398a7377ac4dbab5ed3add3cbbe9a1bea538a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 9 Nov 2014 20:05:55 +0100
Subject: Adding test for bug 3792.

---
 test-suite/bugs/closed/3792.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/3792.v

diff --git a/test-suite/bugs/closed/3792.v b/test-suite/bugs/closed/3792.v
new file mode 100644
index 0000000000..39057b9c52
--- /dev/null
+++ b/test-suite/bugs/closed/3792.v
@@ -0,0 +1,4 @@
+Fail Definition pull_if_dep
+: forall {A} (P : bool -> Type) (a : A true) (a' : A false)
+         (b : bool),
+    P (if b as b return A b then a else a').
-- 
cgit v1.2.3