diff --git a/README.md b/README.md
index f0147cc55f1b164b9f5337572b0e24acb82ec809..b211567a0bf0187e70c5c1ca740eacf7f83fecf1 100644
--- a/README.md
+++ b/README.md
@@ -20,6 +20,20 @@ The key features of this library are as follows:
   `set_solver` for goals involving set operations.
 - It is entirely dependency- and axiom-free.
 
+## Side-effects
+
+Importing std++ has some side effects as the library sets some global options.
+Notably:
+
+* `Generalizable All Variables`: This option enables implicit generalization in
+  arguments of the form `` `{...}`` (i.e., anonymous arguments).  Unfortunately, it
+  also enables implicit generalization in `Instance`.  We think that the fact
+  taht both behaviors are coupled together is a
+  [bug in Coq](https://github.com/coq/coq/issues/6030).
+* The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
+  `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`.  See
+  [`base.v`](`theories/base.v`) for further details.
+
 ## History
 
 Coq-std++ has originally been developed by Robbert Krebbers as part of his
diff --git a/theories/base.v b/theories/base.v
index 3570aae7cad56e64c37f66c2f1896dc18ec0e21e..248b48cf07e1d18d2fab1d760ea0318e506f5a24 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -4,12 +4,20 @@
 that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, collections, and various other data
 structures. *)
-Global Generalizable All Variables.
+
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
 Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 
+(** Enable implicit generalization. *)
+(* This option enables implicit generalization in arguments of the form
+   `{...} (i.e., anonymous arguments).  Unfortunately, it also enables
+   implicit generalization in `Instance`.  We think that the fact taht both
+   behaviors are coupled together is a [bug in
+   Coq](https://github.com/coq/coq/issues/6030). *)
+Global Generalizable All Variables.
+
 (** * Tweak program *)
 (** 1. Since we only use Program to solve logical side-conditions, they should
 always be made Opaque, otherwise we end up with performance problems due to