Merge branch 'ralf/options' into 'master'

re-export std++ options

See merge request iris/iris!922

CHANGELOG.md

@@ -7,6 +7,13 @@ lemma.
 
 Coq 8.13 is no longer supported.
 
+**Changes in `prelude`:**
+
+* Re-export `stdpp.options` from `iris.prelude.options`. This enables 'light'
+  name mangling, which prefixes auto-generated names with `__`. This only
+  affects developments that explicitly opt-in to following the Iris
+  configuration by importing `iris.prelude.options`.
+
 **Changes in `algebra`:**
 
 * Add (basic) support for `gset` and `gset_disj` cameras to `set_solver`.
@@ -97,6 +104,9 @@ Coq 8.13 is no longer supported.
 
 **Changes in `base_logic`:**
 
+* Add `mono_Z` library for monotone non-negative integers.
+  (This has exactly the same lemmas as `mono_nat`. It is useful in cases
+  where one wants to avoid `nat` entirely and use `Z` throughout.)
 * Add `IsExcept0` instance for invariants, allowing you to remove laters of
   timeless hypotheses when proving an invariant (without an update).
 * Make `uPred.unseal` tactic more robust by using types to unfold the right
@@ -115,12 +125,6 @@ Coq 8.13 is no longer supported.
   postcondition into the context via `as (x1 ... xn) "ipat1 ... ipatn"`.
 * Add comparison `≤` and `<` for locations. (by Arthur Azevedo de Amorim).
 
-**Changes in `base_logic`:**
-
-* Add `mono_Z` library for monotone non-negative integers.
-  (This has exactly the same lemmas as `mono_nat`. It is useful in cases
-  where one wants to avoid `nat` entirely and use `Z` throughout.)
-
 **LaTeX changes:**
 
 - Rename `\Alloc` to `\AllocN` and `\Ref` to `\Alloc` for better consistency

iris/prelude/options.v

@@ -2,14 +2,10 @@
 (* 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. *)
+From stdpp Require Export options.
 
-Export Set Default Proof Using "Type".
 Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
 
-(* Enforces that every tactic is executed with a single focused goal, meaning
-that bullets and curly braces must be used to structure the proof. *)
-Export Set Default Goal Selector "!".
-
 (* We always annotate hints with locality ([Global] or [Local]). This enforces
 that at least global hints are annotated. *)
 Export Set Warnings "+deprecated-hint-without-locality".