From 6b223d1d668ecb76aa2609b7d6bb8a19e13136cd Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 9 May 2020 13:39:34 -0400
Subject: Revert "[with_strategy] Fix for coqchk"

This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18.

We instead add a warning in the manual and a kludge in the test-suite.
---
 test-suite/success/with_strategy.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index e0d0252a47..077b57c87f 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -572,3 +572,6 @@ Goal id 0 = 0.
                                    (assert_succeeds unfold_id))))))))))).
   reflexivity.
 Qed.
+
+(* Fake out coqchk to work around what is essentially COQBUG(https://github.com/coq/coq/issues/12200) *)
+Reset Initial.
-- 
cgit v1.2.3