From adb9363ca250bc52c6ae004951d6ded79a5ac529 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 16 Sep 2020 15:17:47 +0200
Subject: [PATCH] also Set Default Goal Selector

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

diff --git a/theories/options.v b/theories/options.v
index fa046af6..7e385685 100644
--- a/theories/options.v
+++ b/theories/options.v
@@ -4,6 +4,9 @@ file is *imported*, the option will only apply on the import site
 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 "!".
 
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.
-- 
GitLab