diff --git a/Makefile b/Makefile
index 877492275c72e88614c432f7b316b85b513137dc..8de6ba818504a6f83f508569ffd03a38689cab4c 100644
--- a/Makefile
+++ b/Makefile
@@ -3,9 +3,6 @@ ifeq ($(Y), 1)
 	YFLAG=-y
 endif
 
-# Configure Coq warnings
-COQ_MAKEFILE_FLAGS ?= -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	+@make -f Makefile.coq $@
diff --git a/_CoqProject b/_CoqProject
index a7869b1351ef752e6797dcbc94d5d18a0f6c1e7f..77dae218b59db79e5f330858bf3e44e9c8a5bff9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,7 @@
 -Q theories stdpp
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+-arg -l -arg stdpp_options
+theories/stdpp_options.v
 theories/option.v
 theories/fin_map_dom.v
 theories/bset.v
diff --git a/theories/base.v b/theories/base.v
index 65233ddfe3a3be343c6437f242577bc10dbd6936..6c2b35be19d0f34d7fac90c4af20d86c4dd516e8 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -4,15 +4,10 @@
 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.
-Global Set Automatic Coercions Import.
-Global Set Asymmetric Patterns.
-Global Unset Transparent Obligations.
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
 Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
-Obligation Tactic := idtac.
 
 (** Sealing off definitions *)
 Set Primitive Projections.
diff --git a/theories/stdpp_options.v b/theories/stdpp_options.v
new file mode 100644
index 0000000000000000000000000000000000000000..b2b008674d3c07776ee52db949fe9eea20e92171
--- /dev/null
+++ b/theories/stdpp_options.v
@@ -0,0 +1,5 @@
+Generalizable All Variables.
+Set Automatic Coercions Import.
+Set Asymmetric Patterns.
+Unset Transparent Obligations.
+Obligation Tactic := idtac.