diff --git a/.gitignore b/.gitignore
index 8c0aeb806b09cd18a1faa17752aef4261f947f0f..c9a7505f2ba41bd9e8a03a542c07a5d9ce1a7a08 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,5 +17,5 @@
 .#*
 auto
 *.fmt
-coq/*/Makefile.coq
+Makefile.coq*
 *~
diff --git a/coq/ra/Makefile b/Makefile
similarity index 82%
rename from coq/ra/Makefile
rename to Makefile
index 5971295f25b9d782747ca671b6b1042d595989dd..7bfa06f89a5c19f9b279f65875196f870b6f88c7 100644
--- a/coq/ra/Makefile
+++ b/Makefile
@@ -12,7 +12,7 @@ all: Makefile.coq
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
-	find \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
+	find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
 	rm -f Makefile.coq
 
 # Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
@@ -22,9 +22,9 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
 
 # Install build-dependencies
 build-dep:
-	../build/opam-pins.sh < ../../opam.pins
+	build/opam-pins.sh < opam.pins
 	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
-	opam pin add opam-builddep-temp "$$(pwd)/../..#HEAD" -k git -n -y
+	opam pin add opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
 	opam install opam-builddep-temp --deps-only $(YFLAG)
 	opam pin remove opam-builddep-temp
 
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000000000000000000000000000000000000..1f56b6dd9bbf2373374a7c44f36480955e4849d0
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1,73 @@
+-Q theories igps
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+theories/iris_lemmas.v
+theories/arith.v
+theories/infrastructure.v
+theories/types.v
+theories/proofmode.v
+theories/machine.v
+theories/history.v
+theories/lifting.v
+theories/lang.v
+theories/tactics.v
+theories/wp_tactics.v
+theories/derived.v
+theories/notation.v
+theories/blocks_generic.v
+theories/blocks.v
+theories/malloc.v
+theories/persistor.v
+theories/fractor.v
+theories/viewpred.v
+theories/weakestpre.v
+theories/bigop.v
+theories/abs_view.v
+theories/escrows.v
+theories/rsl_sts.v
+theories/rsl.v
+theories/rsl_instances.v
+theories/base/ghosts.v
+theories/base/helpers.v
+theories/base/accessors.v
+theories/base/at_shared.v
+theories/base/na_shared.v
+theories/base/fork.v
+theories/base/alloc.v
+theories/base/dealloc.v
+theories/base/na_read.v
+theories/base/na_write.v
+theories/na.v
+theories/base/at_read.v
+theories/base/at_write.v
+theories/base/at_cas.v
+theories/base/at_fai.v
+theories/base/atomic.v
+theories/base/base.v
+theories/adequacy.v
+theories/gps/shared.v
+theories/gps/init.v
+theories/gps/read.v
+theories/gps/write.v
+theories/gps/cas.v
+theories/gps/fai.v
+theories/gps/raw.v
+theories/gps/inst_shared.v
+theories/gps/plain.v
+theories/gps/singlewriter.v
+theories/gps/fractional.v
+theories/gps/recursive.v
+theories/examples/repeat.v
+theories/examples/nat_tokens.v
+theories/examples/unit_token.v
+theories/examples/message_passing_base.v
+theories/examples/protocols.v
+theories/examples/message_passing.v
+theories/examples/spin_lock.v
+theories/examples/circ_buffer.v
+theories/examples/ticket_lock.v
+theories/examples/tstack.v
+theories/examples/msqueue.v
+theories/examples/sc_stack.v
+theories/examples/rcu_data.v
+theories/examples/rcu.v
+theories/tests/message_passing.v
diff --git a/coq/ra/awk.Makefile b/awk.Makefile
similarity index 100%
rename from coq/ra/awk.Makefile
rename to awk.Makefile
diff --git a/coq/build/opam-ci.sh b/build/opam-ci.sh
similarity index 100%
rename from coq/build/opam-ci.sh
rename to build/opam-ci.sh
diff --git a/coq/build/opam-pins.sh b/build/opam-pins.sh
similarity index 100%
rename from coq/build/opam-pins.sh
rename to build/opam-pins.sh
diff --git a/coq/ra/_CoqProject b/coq/ra/_CoqProject
deleted file mode 100644
index b2daa55833f36ad12c2d85c2f9fd212116b0aaa9..0000000000000000000000000000000000000000
--- a/coq/ra/_CoqProject
+++ /dev/null
@@ -1,73 +0,0 @@
--R . ra
--arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-./iris_lemmas.v
-./arith.v
-./infrastructure.v
-./types.v
-./proofmode.v
-./machine.v
-./history.v
-./lifting.v
-./lang.v
-./tactics.v
-./wp_tactics.v
-./derived.v
-./notation.v
-./blocks_generic.v
-./blocks.v
-./malloc.v
-./persistor.v
-./fractor.v
-./viewpred.v
-./weakestpre.v
-./bigop.v
-./abs_view.v
-./escrows.v
-./rsl_sts.v
-./rsl.v
-./rsl_instances.v
-base/ghosts.v
-base/helpers.v
-base/accessors.v
-base/at_shared.v
-base/na_shared.v
-base/fork.v
-base/alloc.v
-base/dealloc.v
-base/na_read.v
-base/na_write.v
-na.v
-base/at_read.v
-base/at_write.v
-base/at_cas.v
-base/at_fai.v
-base/atomic.v
-base/base.v
-adequacy.v
-gps/shared.v
-gps/init.v
-gps/read.v
-gps/write.v
-gps/cas.v
-gps/fai.v
-gps/raw.v
-gps/inst_shared.v
-gps/plain.v
-gps/singlewriter.v
-gps/fractional.v
-gps/recursive.v
-examples/repeat.v
-examples/nat_tokens.v
-examples/unit_token.v
-examples/message_passing_base.v
-examples/protocols.v
-examples/message_passing.v
-examples/spin_lock.v
-examples/circ_buffer.v
-examples/ticket_lock.v
-examples/tstack.v
-examples/msqueue.v
-examples/sc_stack.v
-examples/rcu_data.v
-examples/rcu.v
-tests/message_passing.v
diff --git a/coq/ra/base/atomic.v b/coq/ra/base/atomic.v
deleted file mode 100644
index 56e2be037615d0c352586df08cc6f889754e65a2..0000000000000000000000000000000000000000
--- a/coq/ra/base/atomic.v
+++ /dev/null
@@ -1 +0,0 @@
-From ra.base Require Export at_read at_write at_cas at_fai.
\ No newline at end of file
diff --git a/coq/ra/base/base.v b/coq/ra/base/base.v
deleted file mode 100644
index e1023b434af978dce4ebbb1b2affd86953028f11..0000000000000000000000000000000000000000
--- a/coq/ra/base/base.v
+++ /dev/null
@@ -1 +0,0 @@
-From ra.base Require Export atomic alloc dealloc accessors fork.
\ No newline at end of file
diff --git a/coq/ra/gps/raw.v b/coq/ra/gps/raw.v
deleted file mode 100644
index 9c41a656a0c644298ccd54002bee0df9417a55a2..0000000000000000000000000000000000000000
--- a/coq/ra/gps/raw.v
+++ /dev/null
@@ -1 +0,0 @@
-From ra.gps Require Export shared init read write cas fai.
\ No newline at end of file
diff --git a/opam b/opam
index 8d6cdca9527ecb35e5f3dcb7249619bf4e3d339b..b3dba1e7390df87e86b1e40f6a76a77c5c2e1548 100644
--- a/opam
+++ b/opam
@@ -1,5 +1,5 @@
 opam-version: "1.2"
-name: "coq-gps"
+name: "coq-igps"
 version: "dev"
 maintainer: "Jan-Oliver Kaiser, Hoang-Hai Dang"
 authors: "Jan-Oliver Kaiser, Hoang-Hai Dang"
@@ -10,9 +10,7 @@ build: [
   [make "-j%{jobs}%"]
 ]
 install: [make "install"]
-# TODO: probably we want to install things to a different folder, "ra" is rather undescriptive
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/ra" ]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
-  "coq-iris" #{ = "3.0.0" }
-  "coq-stdpp"
+  "coq-iris"
 ]
diff --git a/coq/ra/abs_view.v b/theories/abs_view.v
similarity index 97%
rename from coq/ra/abs_view.v
rename to theories/abs_view.v
index 19805a0ef45540ed6cebecaa972a617285c0057b..67aa5d5b81ca196ad44d7372caa71c3cf367ce1c 100644
--- a/coq/ra/abs_view.v
+++ b/theories/abs_view.v
@@ -3,8 +3,8 @@ From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import viewpred proofmode.
-From ra.base Require Import ghosts.
+From igps Require Import viewpred proofmode.
+From igps.base Require Import ghosts.
 
 
 Class absViewG Σ := AbsViewG {
diff --git a/coq/ra/adequacy.v b/theories/adequacy.v
similarity index 99%
rename from coq/ra/adequacy.v
rename to theories/adequacy.v
index b1d2c547c7fdd63dbe1bb9df1b1fa7e0496bab4a..5ce53a9d21e48131cb2732b373442976ae64f7bf 100644
--- a/coq/ra/adequacy.v
+++ b/theories/adequacy.v
@@ -3,8 +3,8 @@ From iris.base_logic Require Import lib.invariants big_op.
 From iris.algebra Require Import auth.
 Set Default Proof Using "Type".
 
-From ra Require Import lang weakestpre proofmode.
-From ra.base Require Import ghosts.
+From igps Require Import lang weakestpre proofmode.
+From igps.base Require Import ghosts.
 
 Class basePreG Σ := BasePreG {
   base_preG_iris :> ownPPreG (ra_lang) Σ;
diff --git a/coq/ra/arith.v b/theories/arith.v
similarity index 100%
rename from coq/ra/arith.v
rename to theories/arith.v
diff --git a/coq/ra/base/accessors.v b/theories/base/accessors.v
similarity index 98%
rename from coq/ra/base/accessors.v
rename to theories/base/accessors.v
index 49b349ad7e987c4e4d2895d1d2ad6d4843c714dd..4f188fe974dc423055378225974c8148b788d344 100644
--- a/coq/ra/base/accessors.v
+++ b/theories/base/accessors.v
@@ -2,8 +2,8 @@ From iris.base_logic Require Export lib.invariants lib.viewshifts.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth excl gmap.
 
-From ra Require Import infrastructure machine lang history.
-From ra Require Export ghosts.
+From igps Require Import infrastructure machine lang history.
+From igps Require Export ghosts.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/base/alloc.v b/theories/base/alloc.v
similarity index 98%
rename from coq/ra/base/alloc.v
rename to theories/base/alloc.v
index f18e163e9bd7725a27075549610c26f7b76bb537..a8aa56cf23a5bb9a02cd7d0b45c73b3295070f0f 100644
--- a/coq/ra/base/alloc.v
+++ b/theories/base/alloc.v
@@ -1,6 +1,6 @@
-From ra Require Import lang.
+From igps Require Import lang.
 From iris.proofmode Require Import tactics.
-From ra.base Require Import ghosts at_shared.
+From igps.base Require Import ghosts at_shared.
 
 Section Alloc.
   Context `{fG : !foundationG Σ}.
diff --git a/coq/ra/base/at_cas.v b/theories/base/at_cas.v
similarity index 99%
rename from coq/ra/base/at_cas.v
rename to theories/base/at_cas.v
index 305d7939b2d68af23f0393ac74297e4f295da3ee..197acd7efa7fcd0a5f11ae204974967ef9b1d753 100644
--- a/coq/ra/base/at_cas.v
+++ b/theories/base/at_cas.v
@@ -1,4 +1,4 @@
-From ra.base Require Import at_shared.
+From igps.base Require Import at_shared.
 
 Lemma f_CAS `{fG : !foundationG Σ} π V l h (v_r v_w: Z):
   {{{ PSCtx ∗ ▷ Seen π V ∗ ▷ Hist l h ∗ ⌜init_local h V⌝ }}}
diff --git a/coq/ra/base/at_fai.v b/theories/base/at_fai.v
similarity index 99%
rename from coq/ra/base/at_fai.v
rename to theories/base/at_fai.v
index 076b402407e9dbd37438ae86f4a39a5017a5ab26..7c63dfe9d37a0236e156d7c5f113486b9055ae7c 100644
--- a/coq/ra/base/at_fai.v
+++ b/theories/base/at_fai.v
@@ -1,4 +1,4 @@
-From ra.base Require Import at_shared.
+From igps.base Require Import at_shared.
 
 Lemma f_FAI `{fG : !foundationG Σ} C π V l h:
   {{{ PSCtx ∗ ▷ Seen π V ∗ ▷ Hist l h ∗ ⌜init_local h V⌝ }}}
diff --git a/coq/ra/base/at_read.v b/theories/base/at_read.v
similarity index 98%
rename from coq/ra/base/at_read.v
rename to theories/base/at_read.v
index 2d09f3df19dd22e5c3658b61ccc67e15f9db4250..bb8e4ad27ddcfce58a0f4c8c2bb1b58b644cd568 100644
--- a/coq/ra/base/at_read.v
+++ b/theories/base/at_read.v
@@ -1,4 +1,4 @@
-From ra.base Require Import at_shared.
+From igps.base Require Import at_shared.
 
 Lemma f_read_at `{fG : !foundationG Σ} π V_l l h :
   {{{ PSCtx
diff --git a/coq/ra/base/at_shared.v b/theories/base/at_shared.v
similarity index 97%
rename from coq/ra/base/at_shared.v
rename to theories/base/at_shared.v
index d09b44852d7766c7109908fb3201eb72b76e6c99..64a15eedf4906058e4362e7f31c1d7a27e6ce701 100644
--- a/coq/ra/base/at_shared.v
+++ b/theories/base/at_shared.v
@@ -5,8 +5,8 @@ From iris.algebra Require Export auth frac excl gmap.
 
 Import uPred.
 
-From ra Require Export notation.
-From ra.base Require Export accessors helpers ghosts.
+From igps Require Export notation.
+From igps.base Require Export accessors helpers ghosts.
 
 Lemma write_at_update_hist Ï‚ Ï‚' V h t l v (m: message)
   (HOld: h ≡ map_vt (hist_from (mem ς) l t))
diff --git a/coq/ra/base/at_write.v b/theories/base/at_write.v
similarity index 98%
rename from coq/ra/base/at_write.v
rename to theories/base/at_write.v
index d2b1ad49d9c7c4691359ee67392031c0a2baf5ba..217c227a568ae755c20606d2266e068a354f924e 100644
--- a/coq/ra/base/at_write.v
+++ b/theories/base/at_write.v
@@ -1,4 +1,4 @@
-From ra.base Require Import at_shared.
+From igps.base Require Import at_shared.
 
 Lemma f_write_at `{fG : !foundationG Σ} π V_l l h v:
   {{{ PSCtx 
diff --git a/theories/base/atomic.v b/theories/base/atomic.v
new file mode 100644
index 0000000000000000000000000000000000000000..d8a02a7d49027460a1129334d2b54d8db4495980
--- /dev/null
+++ b/theories/base/atomic.v
@@ -0,0 +1 @@
+From igps.base Require Export at_read at_write at_cas at_fai.
\ No newline at end of file
diff --git a/theories/base/base.v b/theories/base/base.v
new file mode 100644
index 0000000000000000000000000000000000000000..f17425082f29f742f0f842d159fdc8c80757e4e0
--- /dev/null
+++ b/theories/base/base.v
@@ -0,0 +1 @@
+From igps.base Require Export atomic alloc dealloc accessors fork.
\ No newline at end of file
diff --git a/coq/ra/base/dealloc.v b/theories/base/dealloc.v
similarity index 98%
rename from coq/ra/base/dealloc.v
rename to theories/base/dealloc.v
index 0307287c01222f7c8aaf78c0e7dc027d9a545a40..6ab0f0c38c7e9c057e1acf789fee9f57c7d4828c 100644
--- a/coq/ra/base/dealloc.v
+++ b/theories/base/dealloc.v
@@ -1,4 +1,4 @@
-From ra.base Require Import na_shared.
+From igps.base Require Import na_shared.
 
 Lemma f_dealloc `{fG : !foundationG Σ} π V_l l h v :
   {{{ PSCtx ∗ ▷ Seen π V_l 
diff --git a/coq/ra/base/fork.v b/theories/base/fork.v
similarity index 97%
rename from coq/ra/base/fork.v
rename to theories/base/fork.v
index 49c7a69a858bad305bca269a27ca0ebd815f1109..a0697debe9299c699cddb3a9bef8f5195394ab84 100644
--- a/coq/ra/base/fork.v
+++ b/theories/base/fork.v
@@ -1,4 +1,4 @@
-From ra.base Require Import na_shared.
+From igps.base Require Import na_shared.
 
 Lemma f_fork `{fG : foundationG Σ} (Φ : val ra_lang → iProp _) (P: iProp _) π V e:
     PSCtx
diff --git a/coq/ra/base/ghosts.v b/theories/base/ghosts.v
similarity index 99%
rename from coq/ra/base/ghosts.v
rename to theories/base/ghosts.v
index 875c68319fb3584b0dd390a5cc516da3eabc7887..1ed9991fff502520ce055aa2296fa169a4e40cfa 100644
--- a/coq/ra/base/ghosts.v
+++ b/theories/base/ghosts.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export ownp.
 From iris.algebra Require Import deprecated.
 Export deprecated.dec_agree.
 From iris.base_logic Require Import big_op lib.invariants.
-From ra Require Import lang history.
+From igps Require Import lang history.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/base/helpers.v b/theories/base/helpers.v
similarity index 98%
rename from coq/ra/base/helpers.v
rename to theories/base/helpers.v
index 51e411b22cae937edc8c8457a83cd4e5d92a6239..39a60f0bd118bc1c62cf9f89200174439ae7a730 100644
--- a/coq/ra/base/helpers.v
+++ b/theories/base/helpers.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Import excl.
 
-From ra Require Import infrastructure machine history lifting.
-From ra Require Export ghosts.
+From igps Require Import infrastructure machine history lifting.
+From igps Require Export ghosts.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/base/na_read.v b/theories/base/na_read.v
similarity index 99%
rename from coq/ra/base/na_read.v
rename to theories/base/na_read.v
index 7552c0349392a8276401cbdc1dfaa9e65b401c5f..95a71e28da989ff66df98e2d0aa963d1cab4ba0e 100644
--- a/coq/ra/base/na_read.v
+++ b/theories/base/na_read.v
@@ -1,4 +1,4 @@
-From ra.base Require Import na_shared.
+From igps.base Require Import na_shared.
 
 Lemma f_read_na `{fG : foundationG Σ} π V_l l h :
   {{{ PSCtx ∗ ▷ Seen π V_l ∗ ▷ Hist l h
diff --git a/coq/ra/base/na_shared.v b/theories/base/na_shared.v
similarity index 95%
rename from coq/ra/base/na_shared.v
rename to theories/base/na_shared.v
index b9e1b635046e5c02ea2d233aaa6b4fd3a842c172..25776422072cfbd0a805d5a4aceee8b9c7df1e06 100644
--- a/coq/ra/base/na_shared.v
+++ b/theories/base/na_shared.v
@@ -5,8 +5,8 @@ From iris.algebra Require Export auth frac excl gmap.
 
 Import uPred.
 
-From ra Require Export notation history proofmode.
-From ra.base Require Export ghosts accessors helpers.
+From igps Require Export notation history proofmode.
+From igps.base Require Export ghosts accessors helpers.
 
 Lemma write_na_update_HInv `{fG : !foundationG Σ}
   Ï‚ Ï‚' (h  h2: History) (l : loc) (m: message) HIST
diff --git a/coq/ra/base/na_write.v b/theories/base/na_write.v
similarity index 98%
rename from coq/ra/base/na_write.v
rename to theories/base/na_write.v
index c006cdbdc52be369baefb403cc313f2475dd3f65..dc259ad938dc61b26849feba5bfec7cfff42569c 100644
--- a/coq/ra/base/na_write.v
+++ b/theories/base/na_write.v
@@ -1,4 +1,4 @@
-From ra.base Require Import na_shared.
+From igps.base Require Import na_shared.
 
 Lemma f_write_na `{fG : !foundationG Σ} π V_l l h v:
   {{{ PSCtx
diff --git a/coq/ra/bigop.v b/theories/bigop.v
similarity index 98%
rename from coq/ra/bigop.v
rename to theories/bigop.v
index 8fef0b9b40a044b66c786ff1c824f010e5598df6..b9ed8ee634596de5a641139f56a8235509a893a4 100644
--- a/coq/ra/bigop.v
+++ b/theories/bigop.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Import big_op lib.iprop lib.fractional.
 From iris.proofmode Require Import tactics.
-From ra Require Import viewpred proofmode.
+From igps Require Import viewpred proofmode.
 
 
 Program Definition Pos2Qp (n: positive) : Qp := mk_Qp (Zpos n) _.
diff --git a/coq/ra/blocks.v b/theories/blocks.v
similarity index 98%
rename from coq/ra/blocks.v
rename to theories/blocks.v
index 6d1fa708e8f5c11c41caff2e2615c53f1372f794..f73ab8fa16dd3620375fa6d4f7a3770a987324a8 100644
--- a/coq/ra/blocks.v
+++ b/theories/blocks.v
@@ -1,5 +1,5 @@
-From ra Require Import blocks_generic types lang.
-From ra.base Require Import ghosts.
+From igps Require Import blocks_generic types lang.
+From igps.base Require Import ghosts.
 
 Section MHist.
   Implicit Type (M : gset message).
diff --git a/coq/ra/blocks_generic.v b/theories/blocks_generic.v
similarity index 99%
rename from coq/ra/blocks_generic.v
rename to theories/blocks_generic.v
index 42da996498a9c5275f2549069dca26d6cdc8adb4..e5cd1e1eadc342a6e3a8c9f6ea71b98aa5ab5485 100644
--- a/coq/ra/blocks_generic.v
+++ b/theories/blocks_generic.v
@@ -3,7 +3,7 @@ From mathcomp Require Import ssreflect.
 From stdpp Require Import gmap.
 From iris.base_logic Require Import big_op lib.iprop.
 From iris.proofmode Require Import tactics.
-From ra Require Import infrastructure.
+From igps Require Import infrastructure.
 
 Section Blocks.
   Context `{Count : Countable A} {R : relation A}
diff --git a/coq/ra/derived.v b/theories/derived.v
similarity index 98%
rename from coq/ra/derived.v
rename to theories/derived.v
index 558daca66de01aa81136736bdfb9cb44f019ee4d..799b099967f17031f9e02e74cd0ebe8dabab2f61 100644
--- a/coq/ra/derived.v
+++ b/theories/derived.v
@@ -1,4 +1,4 @@
-From ra Require Export lifting.
+From igps Require Export lifting.
 
 Import uPred.
 
diff --git a/coq/ra/escrows.v b/theories/escrows.v
similarity index 98%
rename from coq/ra/escrows.v
rename to theories/escrows.v
index bbc3202529ba2d36cc1e89892e1889092721821c..9ee7d5e92d28f8dd48fe905f38922ba8750eb7b5 100644
--- a/coq/ra/escrows.v
+++ b/theories/escrows.v
@@ -3,9 +3,9 @@ From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import viewpred proofmode.
-From ra.base Require Import ghosts.
-From ra Require Export abs_view.
+From igps Require Import viewpred proofmode.
+From igps.base Require Import ghosts.
+From igps Require Export abs_view.
 
 Definition escrowN : namespace := nroot .@ "escrow".
 
diff --git a/coq/ra/examples/circ_buffer.v b/theories/examples/circ_buffer.v
similarity index 98%
rename from coq/ra/examples/circ_buffer.v
rename to theories/examples/circ_buffer.v
index 56f595c38abc3c15f3363842588b676eb27d4254..e2984ec2c2c77614942739a113a016c8c4548f3a 100644
--- a/coq/ra/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -2,10 +2,10 @@ From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import coPset.
 
-From ra Require Export notation malloc escrows bigop.
-From ra Require Import persistor viewpred weakestpre proofmode arith.
-From ra.examples Require Import nat_tokens protocols.
-From ra.gps Require Import singlewriter.
+From igps Require Export notation malloc escrows bigop.
+From igps Require Import persistor viewpred weakestpre proofmode arith.
+From igps.examples Require Import nat_tokens protocols.
+From igps.gps Require Import singlewriter.
 
 Import uPred.
 
diff --git a/coq/ra/examples/message_passing.v b/theories/examples/message_passing.v
similarity index 95%
rename from coq/ra/examples/message_passing.v
rename to theories/examples/message_passing.v
index 361b85d16ff2ac7be64a6be75dc52595e335a56e..7710100ebc791f80fe96b218830a49d38135f59b 100644
--- a/coq/ra/examples/message_passing.v
+++ b/theories/examples/message_passing.v
@@ -2,11 +2,11 @@ From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 
-From ra Require Export malloc repeat notation wp_tactics escrows.
-From ra Require Import persistor viewpred proofmode weakestpre protocols.
-From ra.base Require Import fork.
-From ra.gps Require Import plain.
-From ra.examples Require Import unit_token.
+From igps Require Export malloc repeat notation wp_tactics escrows.
+From igps Require Import persistor viewpred proofmode weakestpre protocols.
+From igps.base Require Import fork.
+From igps.gps Require Import plain.
+From igps.examples Require Import unit_token.
 
 Import uPred.
 
diff --git a/coq/ra/examples/message_passing_base.v b/theories/examples/message_passing_base.v
similarity index 97%
rename from coq/ra/examples/message_passing_base.v
rename to theories/examples/message_passing_base.v
index f32ae78f0ccd5b72d636ad7ed03a223e19453fc8..9e4021490882142487aa267625eb9ae0402ac50a 100644
--- a/coq/ra/examples/message_passing_base.v
+++ b/theories/examples/message_passing_base.v
@@ -3,9 +3,9 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 From iris.base_logic.lib Require Import invariants.
 
-From ra.base Require Import ghosts alloc fork na_write na_read at_write at_read.
-From ra.examples Require Import unit_token.
-From ra Require Export repeat notation wp_tactics proofmode.
+From igps.base Require Import ghosts alloc fork na_write na_read at_write at_read.
+From igps.examples Require Import unit_token.
+From igps Require Export repeat notation wp_tactics proofmode.
 Import uPred.
 
 Definition message_passing : base.expr :=
diff --git a/coq/ra/examples/msqueue.v b/theories/examples/msqueue.v
similarity index 99%
rename from coq/ra/examples/msqueue.v
rename to theories/examples/msqueue.v
index b244e1233df4d94f1f3342d0828625fcb23772ac..f21480b229f8ea00e4d623d46d0a288e82997bf8 100644
--- a/coq/ra/examples/msqueue.v
+++ b/theories/examples/msqueue.v
@@ -1,9 +1,9 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import notation malloc escrows repeat protocols.
-From ra.gps Require Import shared plain recursive.
-From ra.examples Require Import unit_token.
+From igps Require Import notation malloc escrows repeat protocols.
+From igps.gps Require Import shared plain recursive.
+From igps.examples Require Import unit_token.
 Import uPred.
 
 (** Simplified formalization of Michael-Scott queue
diff --git a/coq/ra/examples/nat_tokens.v b/theories/examples/nat_tokens.v
similarity index 98%
rename from coq/ra/examples/nat_tokens.v
rename to theories/examples/nat_tokens.v
index d871e6798117f13c0640d8c793fc9a35e6c5222f..39cd4f0f5a46b5d7573e231b110d91d21cde95f3 100644
--- a/coq/ra/examples/nat_tokens.v
+++ b/theories/examples/nat_tokens.v
@@ -1,7 +1,7 @@
 From Coq Require Import Psatz.
 From iris.algebra Require Import coPset.
 
-From ra Require Import arith infrastructure.
+From igps Require Import arith infrastructure.
 
 (** Tokens with infinite number to be used in various examples **)
 
diff --git a/coq/ra/examples/protocols.v b/theories/examples/protocols.v
similarity index 93%
rename from coq/ra/examples/protocols.v
rename to theories/examples/protocols.v
index a1a49fc8282c5c357012bfd5c3736bb9da8a0d3c..56320748989e33b9e996059c4c9cda264ea2614a 100644
--- a/coq/ra/examples/protocols.v
+++ b/theories/examples/protocols.v
@@ -1,4 +1,4 @@
-From ra.gps Require Export shared.
+From igps.gps Require Export shared.
 
 Canonical Structure natProtocol : protocolT := ProtocolT _ le.
 
diff --git a/coq/ra/examples/rcu.v b/theories/examples/rcu.v
similarity index 99%
rename from coq/ra/examples/rcu.v
rename to theories/examples/rcu.v
index 1dc85fdf53b95310b8893839c36d8be1c41e83c2..72ea64f08b692f5ce117ccaf5384eb2eeeedd184 100644
--- a/coq/ra/examples/rcu.v
+++ b/theories/examples/rcu.v
@@ -3,9 +3,9 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth coPset.
 From iris.base_logic Require Import big_op.
 
-From ra Require Import notation malloc escrows repeat protocols bigop.
-From ra.gps Require Import shared plain fractional singlewriter recursive.
-From ra.examples Require Import sc_stack nat_tokens rcu_data.
+From igps Require Import notation malloc escrows repeat protocols bigop.
+From igps.gps Require Import shared plain fractional singlewriter recursive.
+From igps.examples Require Import sc_stack nat_tokens rcu_data.
 
 Import uPred.
 
diff --git a/coq/ra/examples/rcu_data.v b/theories/examples/rcu_data.v
similarity index 99%
rename from coq/ra/examples/rcu_data.v
rename to theories/examples/rcu_data.v
index 17008d7822bc63885d35467b8708f44c4e19e325..484b398daad6362cfd26a1eb44d0d3bfe439a654 100644
--- a/coq/ra/examples/rcu_data.v
+++ b/theories/examples/rcu_data.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Import iprop own.
 From iris.algebra Require Import auth gmap coPset.
-From ra Require Import infrastructure machine.
+From igps Require Import infrastructure machine.
 
 (** Logical data structure needed for the RCU proof,
       see rcu.v for more info about the original paper *)
diff --git a/coq/ra/examples/repeat.v b/theories/examples/repeat.v
similarity index 97%
rename from coq/ra/examples/repeat.v
rename to theories/examples/repeat.v
index c679a690bbc7365e26f2a094fcbb55f49c7c7b64..6907be7af0089112199799096910bf38d1777b01 100644
--- a/coq/ra/examples/repeat.v
+++ b/theories/examples/repeat.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Import upred primitive derived.
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
-From ra Require Export notation wp_tactics.
+From igps Require Export notation wp_tactics.
 Import uPred.
 
 (* Definition repeat (e: base.expr): base.expr := *)
diff --git a/coq/ra/examples/sc_stack.v b/theories/examples/sc_stack.v
similarity index 99%
rename from coq/ra/examples/sc_stack.v
rename to theories/examples/sc_stack.v
index d686b5b1de306d38934260048ef1eb2d9bc0f432..546dbe139751af50fd9e4030e88056f5d0a3d2bf 100644
--- a/coq/ra/examples/sc_stack.v
+++ b/theories/examples/sc_stack.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import notation malloc na proofmode weakestpre.
+From igps Require Import notation malloc na proofmode weakestpre.
 
 Import uPred.
 
diff --git a/coq/ra/examples/spin_lock.v b/theories/examples/spin_lock.v
similarity index 95%
rename from coq/ra/examples/spin_lock.v
rename to theories/examples/spin_lock.v
index 60fa6b88c950d918ca21e1b413880799cd0aa66c..8a7495999bea5d95a1cdd875dfcdc7401cd411d0 100644
--- a/coq/ra/examples/spin_lock.v
+++ b/theories/examples/spin_lock.v
@@ -2,9 +2,9 @@ From iris.program_logic Require Export weakestpre.
 From iris.base_logic.lib Require Import cancelable_invariants.
 From iris.proofmode Require Import tactics.
 
-From ra Require Export notation malloc repeat wp_tactics viewpred rsl_instances.
-From ra Require Import rsl persistor proofmode weakestpre.
-From ra.base Require Import base.
+From igps Require Export notation malloc repeat wp_tactics viewpred rsl_instances.
+From igps Require Import rsl persistor proofmode weakestpre.
+From igps.base Require Import base.
 Import uPred.
 
 (** Basic spin-lock proven with iRSL *)
diff --git a/coq/ra/examples/ticket_lock.v b/theories/examples/ticket_lock.v
similarity index 99%
rename from coq/ra/examples/ticket_lock.v
rename to theories/examples/ticket_lock.v
index adbb44a0ea6e03e5a84bda490b460ab7fb3a688b..7d4822e85cadf73790499e4264684249b5308a52 100644
--- a/coq/ra/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -3,10 +3,10 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import coPset gmap auth excl.
 From iris.base_logic Require Import big_op.
 
-From ra Require Import escrows notation malloc repeat.
-From ra Require Import persistor viewpred weakestpre proofmode bigop arith.
-From ra.examples Require Import nat_tokens protocols.
-From ra.gps Require Import singlewriter plain recursive.
+From igps Require Import escrows notation malloc repeat.
+From igps Require Import persistor viewpred weakestpre proofmode bigop arith.
+From igps.examples Require Import nat_tokens protocols.
+From igps.gps Require Import singlewriter plain recursive.
 
 (** Formalization of bounded ticket-lock examples.
     The proof is simplified by using single-writer protocols and 
diff --git a/coq/ra/examples/tstack.v b/theories/examples/tstack.v
similarity index 99%
rename from coq/ra/examples/tstack.v
rename to theories/examples/tstack.v
index 5fcbbe759bb2ed364f97fb64fcbcecc278e92601..a6f287f72d4de924f1321e8a9c7c17f44a741c3f 100644
--- a/coq/ra/examples/tstack.v
+++ b/theories/examples/tstack.v
@@ -1,8 +1,8 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import notation malloc repeat protocols.
-From ra.gps Require Import shared plain.
+From igps Require Import notation malloc repeat protocols.
+From igps.gps Require Import shared plain.
 
 Import uPred.
 
diff --git a/coq/ra/examples/unit_token.v b/theories/examples/unit_token.v
similarity index 95%
rename from coq/ra/examples/unit_token.v
rename to theories/examples/unit_token.v
index 0f206b893364119ecc365e685c3eae13582ef700..b8aa3392e8e0d474fe0e6ffeb382bcf49614e130 100644
--- a/coq/ra/examples/unit_token.v
+++ b/theories/examples/unit_token.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 From iris.base_logic.lib Require Import own.
 
-From ra Require Import viewpred.
+From igps Require Import viewpred.
 
 Class uTokG Σ := UnitTokG { init_tokG :> inG Σ (exclR unitC) }.
 Definition uTokΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
diff --git a/coq/ra/fractor.v b/theories/fractor.v
similarity index 99%
rename from coq/ra/fractor.v
rename to theories/fractor.v
index 868eaac8bb976070d60c90e3e1b7ab8d892ffe8b..266847363833f07633ea11c7e37823cd73d92c81 100644
--- a/coq/ra/fractor.v
+++ b/theories/fractor.v
@@ -5,8 +5,8 @@ From iris.base_logic.lib Require Export cancelable_invariants.
 
 Import uPred.
 
-From ra Require Import lang.
-From ra.base Require Import accessors.
+From igps Require Import lang.
+From igps.base Require Import accessors.
 
 Definition fracN : namespace := nroot .@ "fractor".
 
diff --git a/coq/ra/gps/cas.v b/theories/gps/cas.v
similarity index 99%
rename from coq/ra/gps/cas.v
rename to theories/gps/cas.v
index 08754e4478be45a89d994061d6958677fb7aaa4a..6b4abe19f02944c49f19234e9cc8f562192e6960 100644
--- a/coq/ra/gps/cas.v
+++ b/theories/gps/cas.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import at_cas.
+From igps.gps Require Import shared.
+From igps.base Require Import at_cas.
 
 Section CAS.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
diff --git a/coq/ra/gps/fai.v b/theories/gps/fai.v
similarity index 99%
rename from coq/ra/gps/fai.v
rename to theories/gps/fai.v
index ad5500cc8c160bfd442d223e685cc1df1c491550..6d8d50455d80e3e4b432362c5601d18f4eaeb7df 100644
--- a/coq/ra/gps/fai.v
+++ b/theories/gps/fai.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import at_fai.
+From igps.gps Require Import shared.
+From igps.base Require Import at_fai.
 
 Section FAI.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
diff --git a/coq/ra/gps/fractional.v b/theories/gps/fractional.v
similarity index 99%
rename from coq/ra/gps/fractional.v
rename to theories/gps/fractional.v
index e121c2ca76176cf3426fcb8e09cf1e45379e9e17..a476af30f6483f9aec39019c69a64d4d6ea8cd5e 100644
--- a/coq/ra/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
-From ra.gps Require Export inst_shared.
-From ra Require Import abs_view.
+From igps.gps Require Export inst_shared.
+From igps Require Import abs_view.
 
 Section Fractional.
   Context `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF}
diff --git a/coq/ra/gps/init.v b/theories/gps/init.v
similarity index 98%
rename from coq/ra/gps/init.v
rename to theories/gps/init.v
index c2f4fdb068e98dad52f2b1aa4366abce538e3835..f7c0eded04a6de5bbf2e0dda06691bcc8fbe8dec 100644
--- a/coq/ra/gps/init.v
+++ b/theories/gps/init.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import na_write.
+From igps.gps Require Import shared.
+From igps.base Require Import na_write.
 
 Section Init_Strong.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} 
diff --git a/coq/ra/gps/inst_shared.v b/theories/gps/inst_shared.v
similarity index 81%
rename from coq/ra/gps/inst_shared.v
rename to theories/gps/inst_shared.v
index 56d4ba1cb5edbe784ee2d0b8a6592c5c378e4e36..fbe5623a9e9fb8917a5f7963c12a319d56194d23 100644
--- a/coq/ra/gps/inst_shared.v
+++ b/theories/gps/inst_shared.v
@@ -3,9 +3,9 @@ From iris.algebra Require Export auth.
 
 Import uPred.
 
-From ra Require Export persistor fractor proofmode weakestpre viewpred.
-From ra Require Export notation na.
-From ra.gps Require Export raw.
+From igps Require Export persistor fractor proofmode weakestpre viewpred.
+From igps Require Export notation na.
+From igps.gps Require Export raw.
 
 Definition state_sort_eqdec Prtcl {PF : protocol_facts Prtcl} : EqDecision (state_sort Prtcl) := _.
 Notation gps_agreeG Σ Prtcl := (inG Σ (dec_agreeR (EqDecision0 := state_sort_eqdec Prtcl%type) (state_sort Prtcl))).
diff --git a/coq/ra/gps/plain.v b/theories/gps/plain.v
similarity index 99%
rename from coq/ra/gps/plain.v
rename to theories/gps/plain.v
index 81de484cb2c53a7815e37d6bab1298a8eb30659c..13de7c3542469915076846a03fabfa955ee36f35 100644
--- a/coq/ra/gps/plain.v
+++ b/theories/gps/plain.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From ra.gps Require Export inst_shared.
+From igps.gps Require Export inst_shared.
 
 Section Plain.
   Context {Σ : gFunctors} {Prtcl : protocolT} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF}
diff --git a/theories/gps/raw.v b/theories/gps/raw.v
new file mode 100644
index 0000000000000000000000000000000000000000..c2b4a38c312a7c9c1aac5b8593c35bc83cbc16a5
--- /dev/null
+++ b/theories/gps/raw.v
@@ -0,0 +1 @@
+From igps.gps Require Export shared init read write cas fai.
\ No newline at end of file
diff --git a/coq/ra/gps/read.v b/theories/gps/read.v
similarity index 98%
rename from coq/ra/gps/read.v
rename to theories/gps/read.v
index ec61e0e1c457fd2af3753c480d5503b3a8ce471d..837cb6b111bbc24731b259956f1d323a7961873a 100644
--- a/coq/ra/gps/read.v
+++ b/theories/gps/read.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import at_read.
+From igps.gps Require Import shared.
+From igps.base Require Import at_read.
 
 Section Read.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
diff --git a/coq/ra/gps/recursive.v b/theories/gps/recursive.v
similarity index 98%
rename from coq/ra/gps/recursive.v
rename to theories/gps/recursive.v
index 3a9692d6e4f851a8a6651d28426699d49a950232..68b2f5b2aca50044aa894a611b5b3154694d4ee2 100644
--- a/coq/ra/gps/recursive.v
+++ b/theories/gps/recursive.v
@@ -5,9 +5,9 @@ From iris.algebra Require Export cmra_big_op ofe.
 
 Import uPred.
 
-From ra Require Import persistor fractor proofmode weakestpre.
-From ra Require Export notation na.
-From ra.gps Require Import shared inst_shared plain fractional singlewriter.
+From igps Require Import persistor fractor proofmode weakestpre.
+From igps Require Export notation na.
+From igps.gps Require Import shared inst_shared plain fractional singlewriter.
 
 Section RecInterp.
   Context {Σ : gFunctors} (Prtcl : protocolT). 
diff --git a/coq/ra/gps/shared.v b/theories/gps/shared.v
similarity index 98%
rename from coq/ra/gps/shared.v
rename to theories/gps/shared.v
index 2cdd4f2e0028392b2613c55f6ff919757090ab77..6acb1bc99f2525425546fcc2db44e403a6e6adb4 100644
--- a/coq/ra/gps/shared.v
+++ b/theories/gps/shared.v
@@ -2,9 +2,9 @@ From iris.algebra Require Export auth frac excl gmap gset local_updates.
 From iris.program_logic Require Import ectx_lifting.
 From iris.base_logic Require Import lib.sts big_op.
 
-From ra Require Export viewpred tactics notation.
-From ra Require Export blocks_generic blocks proofmode viewpred.
-From ra.base Require Export ghosts.
+From igps Require Export viewpred tactics notation.
+From igps Require Export blocks_generic blocks proofmode viewpred.
+From igps.base Require Export ghosts.
 
 Structure protocolT :=
    ProtocolT {
diff --git a/coq/ra/gps/singlewriter.v b/theories/gps/singlewriter.v
similarity index 99%
rename from coq/ra/gps/singlewriter.v
rename to theories/gps/singlewriter.v
index e1bed844fd4b23dd6ef86e4dbba47e6b21f86816..0412ef6e27796d366b6d065f5af949e17fbed3de 100644
--- a/coq/ra/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
-From ra.gps Require Export inst_shared.
-From ra Require Import bigop abs_view.
+From igps.gps Require Export inst_shared.
+From igps Require Import bigop abs_view.
 
 
 Section Gname_StrongSW.
diff --git a/coq/ra/gps/write.v b/theories/gps/write.v
similarity index 99%
rename from coq/ra/gps/write.v
rename to theories/gps/write.v
index b26c3ca68cddafb3c3f025aa7739880fe980b164..c6b1e7013df5f8e267c50e24da7521b05eda8f69 100644
--- a/coq/ra/gps/write.v
+++ b/theories/gps/write.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import at_write.
+From igps.gps Require Import shared.
+From igps.base Require Import at_write.
 
 Section Write.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
diff --git a/coq/ra/history.v b/theories/history.v
similarity index 99%
rename from coq/ra/history.v
rename to theories/history.v
index d3e8fb805d688bc3139dc9b806b6917ac6119750..ca5b84f48e1c2a9582d6e60adc631e57626419b9 100644
--- a/coq/ra/history.v
+++ b/theories/history.v
@@ -7,7 +7,7 @@ Global Set Asymmetric Patterns.
 Global Set Bullet Behavior "Strict Subproofs".
 From Coq Require Export Utf8.
 
-From ra Require Import infrastructure types machine.
+From igps Require Import infrastructure types machine.
 
 Section History.
   Notation MessageSet := (gset message).
diff --git a/coq/ra/infrastructure.v b/theories/infrastructure.v
similarity index 100%
rename from coq/ra/infrastructure.v
rename to theories/infrastructure.v
diff --git a/coq/ra/iris_lemmas.v b/theories/iris_lemmas.v
similarity index 100%
rename from coq/ra/iris_lemmas.v
rename to theories/iris_lemmas.v
diff --git a/coq/ra/lang.v b/theories/lang.v
similarity index 99%
rename from coq/ra/lang.v
rename to theories/lang.v
index fedfbeaeec6d98e2df62a27b8e139d7c1d53e5ae..9a2f3b7f781bd951f7bed7590161efbe030893bf 100644
--- a/coq/ra/lang.v
+++ b/theories/lang.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export ectx_language ectxi_language.
 From stdpp Require Export strings gmap.
 From iris.algebra Require Import ofe.
 
-From ra Require Export machine.
+From igps Require Export machine.
 
 Module base.
   Open Scope Z_scope.
diff --git a/coq/ra/lifting.v b/theories/lifting.v
similarity index 99%
rename from coq/ra/lifting.v
rename to theories/lifting.v
index 3000bb882eb92a3c7f1386333dafaf620ea6c32f..fec1dc9820f4dafa05b1255398bd0ada458aa715 100644
--- a/coq/ra/lifting.v
+++ b/theories/lifting.v
@@ -4,8 +4,8 @@ From iris.proofmode Require Import tactics.
 
 Import uPred.
 
-From ra Require Import types.
-From ra Require Export lang history tactics.
+From igps Require Import types.
+From igps Require Export lang history tactics.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/machine.v b/theories/machine.v
similarity index 99%
rename from coq/ra/machine.v
rename to theories/machine.v
index e15203d6201375dbe0ef895b250cfb8e3af0b667..bef65df334fa050adb19890c985c5ef944366d7b 100644
--- a/coq/ra/machine.v
+++ b/theories/machine.v
@@ -9,7 +9,7 @@ From Coq Require Export Utf8.
 
 Open Scope positive.
 
-From ra Require Export infrastructure types.
+From igps Require Export infrastructure types.
 
 Notation loc := (positive) (only parsing).
 Section RAMachine.
diff --git a/coq/ra/malloc.v b/theories/malloc.v
similarity index 97%
rename from coq/ra/malloc.v
rename to theories/malloc.v
index c2b48916caf5d1a057adf31937117a0afbd93076..8383cb56b7e6ed2410d4f92fe3d9275b3b06cf69 100644
--- a/coq/ra/malloc.v
+++ b/theories/malloc.v
@@ -3,10 +3,10 @@ From iris.base_logic Require Export lib.invariants.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap.
 
-From ra Require Import weakestpre proofmode.
-From ra Require Export viewpred wp_tactics.
-From ra Require Import notation bigop na.
-From ra.base Require Import ghosts alloc dealloc.
+From igps Require Import weakestpre proofmode.
+From igps Require Export viewpred wp_tactics.
+From igps Require Import notation bigop na.
+From igps.base Require Import ghosts alloc dealloc.
 
 Definition mdealloc : base.val :=
   (λ: "l" "n",
diff --git a/coq/ra/na.v b/theories/na.v
similarity index 98%
rename from coq/ra/na.v
rename to theories/na.v
index f32f133db16fdd72307e86a150d8306ad4b19384..96474c05ccefe9ce550d3d3253118e8fba626bfe 100644
--- a/coq/ra/na.v
+++ b/theories/na.v
@@ -2,9 +2,9 @@ From iris.program_logic Require Import weakestpre.
 From iris.base_logic Require Import lib.invariants.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import viewpred proofmode weakestpre fractor abs_view.
-From ra Require Export notation bigop.
-From ra.base Require Export ghosts na_read na_write.
+From igps Require Import viewpred proofmode weakestpre fractor abs_view.
+From igps Require Export notation bigop.
+From igps.base Require Export ghosts na_read na_write.
 
 Section Helpers.
   Context {Σ : gFunctors}.
diff --git a/coq/ra/notation.v b/theories/notation.v
similarity index 99%
rename from coq/ra/notation.v
rename to theories/notation.v
index 6de027a50be235bc2423359a16741ae858b1de94..3cc4be4ee01f7de170c749c31e8086148a3433c6 100644
--- a/coq/ra/notation.v
+++ b/theories/notation.v
@@ -1,4 +1,4 @@
-From ra Require Export derived.
+From igps Require Export derived.
 Export ra_lang.
 
 Coercion LitInt : Z >-> base_lit.
diff --git a/coq/ra/persistor.v b/theories/persistor.v
similarity index 98%
rename from coq/ra/persistor.v
rename to theories/persistor.v
index c492154715b86ed177f5a8aae2a11869b53333ad..39c66a7191a3ddb24caac7f81e08f7b31cd4445c 100644
--- a/coq/ra/persistor.v
+++ b/theories/persistor.v
@@ -4,9 +4,9 @@ From iris.algebra Require Import auth frac excl gmap.
 
 Import uPred.
 
-From ra Require Import iris_lemmas.
-From ra Require Export lang.
-From ra.base Require Import accessors.
+From igps Require Import iris_lemmas.
+From igps Require Export lang.
+From igps.base Require Import accessors.
 
 Definition persistN : namespace := nroot .@ "persistor".
 Notation persist_invN := (persistN .@ "inv").
diff --git a/coq/ra/proofmode.v b/theories/proofmode.v
similarity index 98%
rename from coq/ra/proofmode.v
rename to theories/proofmode.v
index de307ea8423d5c42d6209ac896f9e0ae1856ad27..c9223d2aabded75e4219204adf0e1e22bfdc6559 100644
--- a/coq/ra/proofmode.v
+++ b/theories/proofmode.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Import iprop.
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Export tactics.
-From ra Require Import viewpred.
+From igps Require Import viewpred.
 
 Section Instances.
   Context {Σ : gFunctors}.
diff --git a/coq/ra/rsl.v b/theories/rsl.v
similarity index 99%
rename from coq/ra/rsl.v
rename to theories/rsl.v
index 4913a7196f1c86551aee685a82e86fc1eee63b03..b1c189335016c0e620e961b4562afc9e458f1d3e 100644
--- a/coq/ra/rsl.v
+++ b/theories/rsl.v
@@ -8,9 +8,9 @@ From iris.proofmode Require Import tactics.
 
 Import uPred.
 
-From ra Require Export lang blocks iris_lemmas.
-From ra Require Import rsl_sts notation viewpred na.
-From ra.base Require Import base.
+From igps Require Export lang blocks iris_lemmas.
+From igps Require Import rsl_sts notation viewpred na.
+From igps.base Require Import base.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/rsl_instances.v b/theories/rsl_instances.v
similarity index 99%
rename from coq/ra/rsl_instances.v
rename to theories/rsl_instances.v
index 8f3b532e77eece00008a32a13a60f71de2c9782b..59bea7cfcaf31c09d86efa9d6b4a115e024c6f91 100644
--- a/coq/ra/rsl_instances.v
+++ b/theories/rsl_instances.v
@@ -7,8 +7,8 @@ From iris.proofmode Require Import tactics.
 
 Import uPred.
 
-From ra Require Export notation viewpred.
-From ra Require Import rsl fractor persistor na proofmode weakestpre.
+From igps Require Export notation viewpred.
+From igps Require Import rsl fractor persistor na proofmode weakestpre.
 
 Section proof.
 
diff --git a/coq/ra/rsl_sts.v b/theories/rsl_sts.v
similarity index 99%
rename from coq/ra/rsl_sts.v
rename to theories/rsl_sts.v
index 4c538956e0f9a417065253d8e37c8a0b12c1b29e..572aed9ab931d1c7a7fe24dc787662518d9fb54c 100644
--- a/coq/ra/rsl_sts.v
+++ b/theories/rsl_sts.v
@@ -2,8 +2,8 @@ From iris.algebra Require Import sts.
 From iris.base_logic.lib Require Import own.
 From stdpp Require Export gmap.
 
-From ra Require Import types infrastructure.
-From ra.base Require Export ghosts.
+From igps Require Import types infrastructure.
+From igps.base Require Export ghosts.
 
 Implicit Types (I : gset gname) (h: History) (i: gname).
 
diff --git a/coq/ra/tactics.v b/theories/tactics.v
similarity index 99%
rename from coq/ra/tactics.v
rename to theories/tactics.v
index 7d4f6912bfa7e97607fff7a7965352ecd9f9d38a..84c47f9d9784820915d84a9efe1443bccc13d94e 100644
--- a/coq/ra/tactics.v
+++ b/theories/tactics.v
@@ -1,4 +1,4 @@
-From ra Require Export lang.
+From igps Require Export lang.
 From stdpp Require Import fin_maps.
 Import base ra_lang.
 
diff --git a/coq/ra/tests/message_passing.v b/theories/tests/message_passing.v
similarity index 87%
rename from coq/ra/tests/message_passing.v
rename to theories/tests/message_passing.v
index 31e61ee4619638ccda7286e3377eb03a57c888ad..1b440aac1c6122d2e2e07438284a29aefcb8d1e1 100644
--- a/coq/ra/tests/message_passing.v
+++ b/theories/tests/message_passing.v
@@ -1,6 +1,6 @@
-From ra.examples Require Import message_passing unit_token.
-From ra.gps Require Import shared inst_shared.
-From ra Require Import adequacy.
+From igps.examples Require Import message_passing unit_token.
+From igps.gps Require Import shared inst_shared.
+From igps Require Import adequacy.
 
 Let Σ : gFunctors := #[ baseΣ;
                         gpsΣ protocols.boolProtocol _ ;
diff --git a/coq/ra/types.v b/theories/types.v
similarity index 98%
rename from coq/ra/types.v
rename to theories/types.v
index 1027675604b0db9f97e30027f2f174f4c7e6c8a6..0bdeeb544d53dd365b8ff31ef8c789c2daf21fec 100644
--- a/coq/ra/types.v
+++ b/theories/types.v
@@ -1,6 +1,6 @@
 From Coq Require Export Utf8.
 From stdpp Require Export gmap finite.
-From ra Require Import infrastructure.
+From igps Require Import infrastructure.
 
 Reserved Notation "'<' x → v @ t , R >" (at level 20, format "< x → v @ t , R >",
                                          x at level 21, v at level 21, t at level 21, R at level 21).
diff --git a/coq/ra/viewpred.v b/theories/viewpred.v
similarity index 99%
rename from coq/ra/viewpred.v
rename to theories/viewpred.v
index 1b899b4945a74cadb44e7a2c8e9e5f3c671c0f04..79dad232d80149e7a2e03dadc3b5d3038b71c24d 100644
--- a/coq/ra/viewpred.v
+++ b/theories/viewpred.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base.
 From iris.base_logic.lib Require Import viewshifts.
 From iris.proofmode Require Import tactics.
-From ra Require Export infrastructure types.
+From igps Require Export infrastructure types.
 
 Canonical Structure View_ofe : ofeT := leibnizC View.
 
diff --git a/coq/ra/weakestpre.v b/theories/weakestpre.v
similarity index 99%
rename from coq/ra/weakestpre.v
rename to theories/weakestpre.v
index 368bf27c2ef30cefc421c48c57af1ac3b5dfc5e0..e6a67d8809c9381f3a90f3ce0aec66429b1f2826 100644
--- a/coq/ra/weakestpre.v
+++ b/theories/weakestpre.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import weakestpre.
-From ra Require Import lang viewpred.
-From ra.base Require Import ghosts.
+From igps Require Import lang viewpred.
+From igps.base Require Import ghosts.
 
 (* Section WeakestPre. *)
 (*   Context `{foundationG Σ}. *)
diff --git a/coq/ra/wp_tactics.v b/theories/wp_tactics.v
similarity index 99%
rename from coq/ra/wp_tactics.v
rename to theories/wp_tactics.v
index 8608952db9bb9be2695adcba81f41c7325164dc8..40d81b81487c6fe51a5bd0a8f34aa0db336706d2 100644
--- a/coq/ra/wp_tactics.v
+++ b/theories/wp_tactics.v
@@ -1,4 +1,4 @@
-From ra Require Export tactics derived.
+From igps Require Export tactics derived.
 Import uPred.
 
 (** wp-specific helper tactics *)