Compare revisions

fa344cbe · fa344cbe · fa344cbe · fa344cbe · fa344cbe · fa344cbe
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
--- a/iris/base_logic/base_logic.v
+++ b/iris/base_logic/base_logic.v
+From iris.bi Require Export bi.
+From iris.base_logic Require Export derived proofmode algebra.
+From iris.prelude Require Import options.
+
+(* The trick of having multiple [uPred] modules, which are all exported in
+another [uPred] module is by Jason Gross and described in:
+https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00069.html *)
+Module Import uPred.
+  Export base_logic.bi.uPred.
+  Export derived.uPred.
+  Export bi.bi.
+End uPred.
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
--- a/iris/base_logic/bupd_alt.v
+++ b/iris/base_logic/bupd_alt.v
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
No results found