diff --git a/theories/base.v b/theories/base.v
index a3a8d2759fff859f1e731bd0e5bb7e2080dba787..117172ef2bbeba5c185ed033c5678a8ea74cfaa0 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