From bc947bd505c1de9b1e4882b8c75a34ebe7a4b053 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Feb 2018 09:05:52 +0100
Subject: [PATCH] Test case for performance regression akin to #153.

Fixed by stdpp 93b4ec70e13a573a9055a5bf1269f5885e18e843.
---
 theories/tests/proofmode.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index aa433d1c8..910aedffc 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -311,6 +311,10 @@ Proof.
   done.
 Qed.
 
+Lemma test_iNext_fail P Q a b c d e f g h i j:
+  ▷^(a + b) ▷^(c + d + e) P -∗ ▷^(f + g + h + i + j) True.
+Proof. iIntros "H". iNext. done. Qed.
+
 Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : uPred M.
 Proof.
   iIntros (H).
-- 
GitLab