From d0fdaa32995e9e8c04ead77bf5e0c1ea57dd01ea Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 May 2023 20:33:01 +0200
Subject: [PATCH] warn users against importing the options file

---
 iris/prelude/options.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/iris/prelude/options.v b/iris/prelude/options.v
index 39f1f4228..80f9b75bf 100644
--- a/iris/prelude/options.v
+++ b/iris/prelude/options.v
@@ -1,4 +1,10 @@
-(** Coq configuration for Iris (not meant to leak to clients) *)
+(** Coq configuration for Iris (not meant to leak to clients).
+If you are a user of Iris, note that importing this file means
+you are implicitly opting-in to every new option we will add here
+in the future. We are *not* guaranteeing any kind of stability here.
+Instead our advice is for you to have your own options file; then
+you can re-export the Iris file there but if we ever add an option
+you disagree with you can easily overwrite it in one central location. *)
 (* 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. *)
-- 
GitLab