From c76d4beae2faa85f02c0adcbb38cc501e615c261 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Aug 2020 18:44:18 +0200
Subject: [PATCH] add options file for library-wide configuration

---
 _CoqProject        | 1 +
 theories/options.v | 5 +++++
 2 files changed, 6 insertions(+)
 create mode 100644 theories/options.v

diff --git a/_CoqProject b/_CoqProject
index f53931331..5cbaf6389 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 000000000..907e59ce4
--- /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".
-- 
GitLab