1 files changed, 11 insertions, 0 deletions
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.