From 87095c3b474e5eae58fe38f0eaee85efbd78488a Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 14 Sep 2020 21:02:05 -0500
Subject: [PATCH] Remove global strict bulleting flag

---
 theories/base.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index a3a8d275..117172ef 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -14,10 +14,6 @@ Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 
-(* TODO: remove this once it's set by an options file (the below command affects
-all transitive users, which we don't want to do) *)
-Global Set Default Goal Selector "!".
-
 (** This notation is necessary to prevent [length] from being printed
 as [strings.length] if strings.v is imported and later base.v. See
 also strings.v and
-- 
GitLab