diff --git a/_CoqProject b/_CoqProject
index f539313315d40a97c29697e99ba5bd5e78faee82..5cbaf6389d77362c6bdf8b8ed583874e3e0a3c54 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,6 +5,7 @@
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
 
+theories/options.v
 theories/algebra/monoid.v
 theories/algebra/cmra.v
 theories/algebra/big_op.v
diff --git a/theories/options.v b/theories/options.v
new file mode 100644
index 0000000000000000000000000000000000000000..907e59ce4882f51fc082477f554139a22b3c497b
--- /dev/null
+++ b/theories/options.v
@@ -0,0 +1,5 @@
+(** Coq configuration for Iris (not meant to leak to clients) *)
+(* Everything here should be [Export Set], which means when this
+file is *imported*, the option will only apply on the import site
+but not transitively. *)
+Export Set Default Proof Using "Type".