From 2ded4c25e532c5dfca0483c211653768ebed01a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Jun 2019 15:39:43 +0200
Subject: UIP in SProp

---
 test-suite/failure/uip_loop.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/failure/uip_loop.v

(limited to 'test-suite/failure')

diff --git a/test-suite/failure/uip_loop.v b/test-suite/failure/uip_loop.v
new file mode 100644
index 0000000000..5b4a88e7cc
--- /dev/null
+++ b/test-suite/failure/uip_loop.v
@@ -0,0 +1,24 @@
+Set Definitional UIP.
+
+Inductive seq {A} (a:A) : A -> SProp :=
+  srefl : seq a a.
+Arguments srefl {_ _}.
+
+(* Axiom implied by propext (so consistent) *)
+Axiom all_eq : forall (P Q:Prop), P -> Q -> seq P Q.
+
+Definition transport (P Q:Prop) (x:P) (y:Q) : Q
+  := match all_eq P Q x y with srefl => x end.
+
+Definition top : Prop := forall P : Prop, P -> P.
+
+Definition c : top :=
+  fun P p =>
+    transport
+      (top -> top)
+      P
+      (fun x : top => x (top -> top) (fun x => x) x)
+      p.
+
+Fail Timeout 1 Eval lazy in c (top -> top) (fun x => x) c.
+(* loops *)
-- 
cgit v1.2.3