Merge PR #10390: UIP in SProp

Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes

1 files changed, 24 insertions, 0 deletions

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 *)