Compare revisions

017605dd · 017605dd · 017605dd · 017605dd · 017605dd · 017605dd
--- 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/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
-From iris.base_logic Require Export derived proofmode.
 From iris.bi Require Export bi.
-Set Default Proof Using "Type".
+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:

--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
--- a/theories/base_logic/bupd_alt.v
+++ b/theories/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/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/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
--- a/iris/base_logic/lib/mono_Z.v
+++ b/iris/base_logic/lib/mono_Z.v
No results found