From ee3b91fe06c72a8ffe92d31a7e40fe54cd71f746 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 25 Apr 2020 13:33:39 -0400
Subject: Elaborate with_strategy warning

As per https://github.com/coq/coq/pull/12129#issuecomment-619389803

Note that we need to work around #12179 in doc of with_strategy
---
 test-suite/success/with_strategy.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index bacea3549f..4f761fb470 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -138,6 +138,17 @@ Goal id 0 = 0.
   reflexivity.
 Time Timeout 5 Defined.
 
+(* test that it works even with [Qed] *)
+Goal id 0 = 0.
+Proof using Type.
+  Time Timeout 5
+       abstract
+       (with_strategy
+          expand [id]
+          assert (id (fact 100) = fact 100) by abstract reflexivity;
+       reflexivity).
+Time Timeout 5 Qed.
+
 (* check that module substitutions happen correctly *)
 Module F.
   Definition id {T} := @id T.
-- 
cgit v1.2.3