From e88e601f03e6930b2fc4a5d1ef7f7da00ce88595 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Sep 2020 11:17:48 +0200
Subject: [PATCH] Default Goal Selector does not work that way on Coq 8.8

---
 theories/options.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/options.v b/theories/options.v
index 7e385685..c94b63dc 100644
--- a/theories/options.v
+++ b/theories/options.v
@@ -6,7 +6,8 @@ but not transitively. *)
 Export Set Default Proof Using "Type".
 (* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
 Export Set Suggest Proof Using. *)
-Export Set Default Goal Selector "!".
+(* FIXME: cannot enable this on Coq 8.8.
+Export Set Default Goal Selector "!". *)
 
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.
-- 
GitLab