diff --git a/_CoqProject b/_CoqProject
index 08cde9de0dc6717e557e896ebb27af4e9a6c7f55..3d556b834a4cd8e22a5e68105d1b422959949494 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -11,39 +11,33 @@
 # We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
 -arg -w -arg -ambiguous-paths
 
-theories/algebra/ordinals/set_model.v
-theories/algebra/ordinals/set_sets.v
-theories/algebra/ordinals/set_functions.v
-theories/algebra/ordinals/set_ordinals.v
-theories/algebra/ordinals/ord_stepindex.v
-theories/algebra/ordinals/arithmetic.v
+theories/prelude/options.v
+theories/prelude/prelude.v
+theories/prelude/classical.v
+
+
+theories/stepindex/stepindex.v
+theories/stepindex/existential_properties.v
+theories/stepindex/ordinals.v
+theories/stepindex/ordinal_arith.v
 
-theories/algebra/base.v
-theories/algebra/stepindex.v
-theories/algebra/monoid.v
 theories/algebra/ofe.v
+theories/algebra/monoid.v
 theories/algebra/cmra.v
 theories/algebra/updates.v
-theories/base_logic/base_logic.v
-theories/program_logic/language.v
-theories/bi/notation.v
-theories/bi/interface.v
-theories/bi/derived_connectives.v
-theories/bi/derived_laws_bi.v
-theories/bi/derived_laws_sbi.v
-theories/bi/satisfiable.v
-
-
 theories/algebra/big_op.v
-theories/algebra/auth.v
-theories/algebra/frac_auth.v
+theories/algebra/cmra_big_op.v
+theories/algebra/numbers.v
+theories/algebra/frac.v
 theories/algebra/gmap.v
+theories/algebra/truncation.v
 theories/algebra/wf_IR.v
 theories/algebra/cofe_solver.v
 theories/algebra/agree.v
 theories/algebra/excl.v
+theories/algebra/view.v
+theories/algebra/auth.v
 theories/algebra/functions.v
-theories/algebra/frac.v
 theories/algebra/csum.v
 theories/algebra/list.v
 theories/algebra/vector.v
@@ -54,62 +48,60 @@ theories/algebra/coPset.v
 theories/algebra/proofmode_classes.v
 theories/algebra/ufrac.v
 theories/algebra/namespace_map.v
-theories/algebra/ufrac_auth.v
 theories/algebra/dfrac.v
-theories/algebra/auth_map.v
-theories/algebra/auth_frac.v
-theories/algebra/mlist.v
-theories/bi/plainly.v
+theories/algebra/lib/excl_auth.v
+theories/algebra/lib/frac_agree.v
+theories/algebra/lib/frac_auth.v
+theories/algebra/lib/gmap_view.v
+theories/algebra/lib/mono_nat.v
+theories/algebra/lib/ufrac_auth.v
+
+theories/bi/notation.v
+theories/bi/interface.v
+theories/bi/derived_connectives.v
+theories/bi/derived_laws.v
+theories/bi/derived_laws_later.v
 theories/bi/big_op.v
-theories/bi/updates.v
+theories/bi/plainly.v
+theories/bi/internal_eq.v
 theories/bi/bi.v
-theories/bi/tactics.v
+theories/bi/updates.v
 theories/bi/embedding.v
-theories/bi/weakestpre.v
+theories/bi/ascii.v
+theories/bi/satisfiable.v
 theories/bi/telescopes.v
 theories/bi/lib/fixpoint.v
 theories/bi/lib/fractional.v
+
 theories/base_logic/upred.v
 theories/base_logic/bi.v
 theories/base_logic/derived.v
+theories/base_logic/algebra.v
 theories/base_logic/proofmode.v
-theories/base_logic/satisfiable.v
+theories/base_logic/base_logic.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
 theories/base_logic/lib/saved_prop.v
 theories/base_logic/lib/wsat.v
 theories/base_logic/lib/invariants.v
 theories/base_logic/lib/fancy_updates.v
-theories/base_logic/lib/logical_step.v
-theories/base_logic/lib/viewshifts.v
+theories/base_logic/lib/satisfiable.v
 theories/base_logic/lib/na_invariants.v
 theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/gen_heap.v
 theories/base_logic/lib/proph_map.v
-theories/program_logic/weakestpre.v
-theories/program_logic/lifting.v
-theories/program_logic/adequacy.v
-theories/program_logic/hoare.v
-theories/program_logic/ectx_language.v
-theories/program_logic/ectxi_language.v
-theories/program_logic/ectx_lifting.v
-theories/program_logic/refinement/ref_source.v
-theories/program_logic/refinement/ref_weakestpre.v
-theories/program_logic/refinement/ref_adequacy.v
-theories/program_logic/refinement/tc_weakestpre.v
-theories/program_logic/refinement/seq_weakestpre.v
-theories/program_logic/refinement/ref_lifting.v
-theories/program_logic/refinement/ref_ectx_lifting.v
-theories/heap_lang/locations.v
-theories/heap_lang/lang.v
-theories/heap_lang/metatheory.v
-theories/heap_lang/tactics.v
-theories/heap_lang/lifting.v
-theories/heap_lang/notation.v
-theories/heap_lang/proofmode.v
-theories/heap_lang/adequacy.v
+
 theories/proofmode/base.v
 theories/proofmode/tokens.v
+theories/proofmode/modalities.v
+theories/proofmode/ident_name.v
+theories/proofmode/classes.v
+theories/proofmode/class_instances.v
+theories/proofmode/class_instances_later.v
+theories/proofmode/class_instances_plainly.v
+theories/proofmode/class_instances_updates.v
+theories/proofmode/class_instances_internal_eq.v
+theories/proofmode/class_instances_embedding.v
 theories/proofmode/coq_tactics.v
 theories/proofmode/ltac_tactics.v
 theories/proofmode/environments.v
@@ -119,53 +111,5 @@ theories/proofmode/spec_patterns.v
 theories/proofmode/sel_patterns.v
 theories/proofmode/tactics.v
 theories/proofmode/notation.v
-theories/proofmode/classes.v
-theories/proofmode/class_instances_bi.v
-theories/proofmode/class_instances_sbi.v
 theories/proofmode/frame_instances.v
-theories/proofmode/modalities.v
 theories/proofmode/modality_instances.v
-
-#################
-### Examples
-#################
-
-# General Transfinite Iris
-theories/examples/transfinite.v
-
-# derived Hoare triples
-theories/examples/refinements/derived.v
-
-# key ideas
-theories/examples/keyideas/simulations.v
-theories/examples/keyideas/generalized_simulations.v
-
-# Existing Safety Examples
-theories/examples/safety/spawn.v
-theories/examples/safety/par.v
-theories/examples/safety/assert.v
-theories/examples/safety/lock.v
-theories/examples/safety/spin_lock.v
-theories/examples/safety/ticket_lock.v
-theories/examples/safety/nondet_bool.v
-theories/examples/safety/counter.v
-theories/examples/safety/lazy_coin.v
-theories/examples/safety/clairvoyant_coin.v 
-
-theories/examples/safety/barrier/barrier.v
-theories/examples/safety/barrier/proof.v
-theories/examples/safety/barrier/specification.v
-theories/examples/safety/barrier/example_client.v
-
-# Termination Proofs
-theories/examples/termination/adequacy.v
-theories/examples/termination/thunk.v
-theories/examples/termination/eventloop.v
-theories/examples/termination/logrel.v
-
-# Termination Preserving Refinement
-theories/examples/refinements/refinement.v
-theories/examples/refinements/memoization.v
-
-# Some formalised counterexamples
-theories/examples/counterexamples.v
diff --git a/opam b/opam
index 8bcc12aef3948a24d81baf3be4eaf846b14d8bce..1f73bac1a2a6adc729b517b7d27902c7787dd735 100644
--- a/opam
+++ b/opam
@@ -10,8 +10,8 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
 synopsis: "This is the Coq development of the Iris Project"
 
 depends: [
-  "coq" { (= "8.10.2") }
-  "coq-stdpp" { (= "1.3.0") }
+  "coq" { (= "8.15.1") }
+  "coq-stdpp" { (= "dev.2022-08-24.0.2c03acaf") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]