diff --git a/_CoqProject b/_CoqProject
index fd0c51064aa623ed614570946cdae3c6d6c50f42..7e78b4c40dd498dbf8c6a11f6e83eb72652e95d4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,5 @@
 # Search paths for all packages. They must all match the regex
 # `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
--Q orc11 orc11
 -Q gpfsl gpfsl
 -Q gpfsl-examples gpfsl.examples
 # silence coq_makefile warning
@@ -12,16 +11,16 @@
 -arg -w -arg -redundant-canonical-projection
 
 # ORC11
-orc11/base.v
-orc11/value.v
-orc11/mem_order.v
-orc11/event.v
-orc11/location.v
-orc11/view.v
-orc11/memory.v
-orc11/tview.v
-orc11/thread.v
-orc11/progress.v
+gpfsl/orc11/base.v
+gpfsl/orc11/value.v
+gpfsl/orc11/mem_order.v
+gpfsl/orc11/event.v
+gpfsl/orc11/location.v
+gpfsl/orc11/view.v
+gpfsl/orc11/memory.v
+gpfsl/orc11/tview.v
+gpfsl/orc11/thread.v
+gpfsl/orc11/progress.v
 
 
 # Language Definitions
diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 078bc0543dc7a378ef95a2ffd77fe26d97048fee..02f1e207625fb991e4c2b34f2dda64ae84468468 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,8 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2024-10-02.2.636308c8") | (= "dev") }
-  "coq-orc11" {= version}
+  "coq-iris"  { (= "dev.2024-10-03.0.4871f965") | (= "dev") }
 ]
 
 build: ["./make-package" "gpfsl" "-j%{jobs}%"]
diff --git a/coq-orc11.opam b/coq-orc11.opam
deleted file mode 100644
index 8e4ad170d18b6d1824483e8e7c48be4e9589e476..0000000000000000000000000000000000000000
--- a/coq-orc11.opam
+++ /dev/null
@@ -1,17 +0,0 @@
-opam-version: "2.0"
-maintainer: "Hoang-Hai Dang <haidang@mpi-sws.org>"
-authors: "The ORC11 semantics team"
-license: "BSD-3-Clause"
-homepage: "https://gitlab.mpi-sws.org/iris/orc11"
-bug-reports: "https://gitlab.mpi-sws.org/iris/orc11/issues"
-dev-repo: "git+https://gitlab.mpi-sws.org/iris/orc11.git"
-version: "dev"
-
-synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
-
-depends: [
-  "coq-stdpp" { (= "dev.2024-10-02.0.2dd41ab5") | (= "dev") }
-]
-
-build: ["./make-package" "orc11" "-j%{jobs}%"]
-install: ["./make-package" "orc11" "install"]
diff --git a/gpfsl-examples/list_helper.v b/gpfsl-examples/list_helper.v
index 531280a3661398d088de1a51261cebb2d4f578db..e1f3f49d9954ab3fbc74f7971fde253e725e2c2c 100644
--- a/gpfsl-examples/list_helper.v
+++ b/gpfsl-examples/list_helper.v
@@ -1,5 +1,5 @@
 From stdpp Require Import numbers sorting.
-From orc11 Require Import base.
+From gpfsl.orc11 Require Import base.
 
 From stdpp Require Import options.
 
diff --git a/gpfsl/algebra/lattice_cmra.v b/gpfsl/algebra/lattice_cmra.v
index 2d9e4aa75bac7d27c05d480b062b2588bffbe3c9..e8d00bd88a550e721231dc6b3564a2905fe64ec5 100644
--- a/gpfsl/algebra/lattice_cmra.v
+++ b/gpfsl/algebra/lattice_cmra.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import cmra auth lib.frac_auth.
 From iris.base_logic.lib Require Import own.
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Require Import iris.prelude.options.
 
diff --git a/gpfsl/gps/block_ends.v b/gpfsl/gps/block_ends.v
index 938ab750b52f9dfff06ea4594730f2eb7949330e..2985ca694a5ec391d3324cf656d83a8af6b123ce 100644
--- a/gpfsl/gps/block_ends.v
+++ b/gpfsl/gps/block_ends.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap.
 From iris.bi Require Import bi big_op.
 
-From orc11 Require Import base.
+From gpfsl.orc11 Require Import base.
 
 Require Import iris.prelude.options.
 
diff --git a/gpfsl/gps/protocols.v b/gpfsl/gps/protocols.v
index 191aab5bc89369e79f724646e1239ea91f42966b..4244ddaa2cb33a610558de15f26cbce3157138b5 100644
--- a/gpfsl/gps/protocols.v
+++ b/gpfsl/gps/protocols.v
@@ -1,4 +1,4 @@
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Record protocolT : Type := {
   pr_stateT     :> Type;
diff --git a/gpfsl/lang/lang.v b/gpfsl/lang/lang.v
index c3f5f361d625f1de01db1a3db54a73ac1e2c0ae1..1db41991085da9bd3a58e526a29c382844e30564 100644
--- a/gpfsl/lang/lang.v
+++ b/gpfsl/lang/lang.v
@@ -2,7 +2,7 @@ From stdpp Require Export binders strings.
 From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.algebra Require Import ofe.
 
-From orc11 Require Export progress.
+From gpfsl.orc11 Require Export progress.
 
 Require Import iris.prelude.options.
 
diff --git a/orc11/base.v b/gpfsl/orc11/base.v
similarity index 100%
rename from orc11/base.v
rename to gpfsl/orc11/base.v
diff --git a/orc11/event.v b/gpfsl/orc11/event.v
similarity index 91%
rename from orc11/event.v
rename to gpfsl/orc11/event.v
index 16b546e4241510ea00bcfc0eb84ab38517d408a4..6c9fc4a4c51fa9ccf4dcc248342e1089a5af1d15 100644
--- a/orc11/event.v
+++ b/gpfsl/orc11/event.v
@@ -1,4 +1,4 @@
-From orc11 Require Export value mem_order.
+From gpfsl.orc11 Require Export value mem_order.
 
 Require Import stdpp.options.
 
diff --git a/orc11/location.v b/gpfsl/orc11/location.v
similarity index 99%
rename from orc11/location.v
rename to gpfsl/orc11/location.v
index b814262fd0ec3d1f45e707ddc472b1090a5adf90..08294a51ed5d05691d2b76332f05aef57aa61443 100644
--- a/orc11/location.v
+++ b/gpfsl/orc11/location.v
@@ -1,5 +1,5 @@
 From stdpp Require Import sorting.
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Require Import stdpp.options.
 
diff --git a/orc11/mem_order.v b/gpfsl/orc11/mem_order.v
similarity index 97%
rename from orc11/mem_order.v
rename to gpfsl/orc11/mem_order.v
index 9cf20a5613db33ddaf65c9ce6d3ba79546c97e03..167d4059d7e745e7602fb06d68bb2e8b138c460c 100644
--- a/orc11/mem_order.v
+++ b/gpfsl/orc11/mem_order.v
@@ -1,4 +1,4 @@
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Require Import stdpp.options.
 
diff --git a/orc11/memory.v b/gpfsl/orc11/memory.v
similarity index 99%
rename from orc11/memory.v
rename to gpfsl/orc11/memory.v
index e7e75d5174bbfa575cde1758b73bab55be6cff67..b1b949c5bef0baa81285320b5398beb99f775ba6 100644
--- a/orc11/memory.v
+++ b/gpfsl/orc11/memory.v
@@ -1,5 +1,5 @@
 From stdpp Require Export gmap finite tactics sorting.
-From orc11 Require Export view value.
+From gpfsl.orc11 Require Export view value.
 
 Require Import stdpp.options.
 
diff --git a/orc11/progress.v b/gpfsl/orc11/progress.v
similarity index 99%
rename from orc11/progress.v
rename to gpfsl/orc11/progress.v
index 6f4e5e6d7d7e907d53406b1e6e0f6960a817b0d2..3fc8d359ee570305ef2a25ec009006d263486e89 100644
--- a/orc11/progress.v
+++ b/gpfsl/orc11/progress.v
@@ -1,5 +1,5 @@
 From stdpp Require Import gmap.
-From orc11 Require Export thread.
+From gpfsl.orc11 Require Export thread.
 
 Require Import stdpp.options.
 
diff --git a/orc11/thread.v b/gpfsl/orc11/thread.v
similarity index 99%
rename from orc11/thread.v
rename to gpfsl/orc11/thread.v
index c9409b8687274f340f2903f29c27983aa220e2f7..8850d957506cf43ccdcd9264fcda24fe00054e34 100644
--- a/orc11/thread.v
+++ b/gpfsl/orc11/thread.v
@@ -1,5 +1,5 @@
 From stdpp Require Import numbers.
-From orc11 Require Export tview event.
+From gpfsl.orc11 Require Export tview event.
 
 Require Import stdpp.options.
 
diff --git a/orc11/tview.v b/gpfsl/orc11/tview.v
similarity index 99%
rename from orc11/tview.v
rename to gpfsl/orc11/tview.v
index 20c46e342d3c2dd3d17958c2a0fbd00875ebaae0..4e329ceb9df7b966cf7197503db89ef444725577 100644
--- a/orc11/tview.v
+++ b/gpfsl/orc11/tview.v
@@ -1,5 +1,5 @@
 From stdpp Require Export gmap tactics.
-From orc11 Require Export view memory mem_order.
+From gpfsl.orc11 Require Export view memory mem_order.
 
 Require Import stdpp.options.
 
diff --git a/orc11/value.v b/gpfsl/orc11/value.v
similarity index 95%
rename from orc11/value.v
rename to gpfsl/orc11/value.v
index 0ab6227433e3d0f8ea8bb07a70b2b9951bdaf76d..fa0596c1d2bcd8b93ce4cd65480f48a2c18f54da 100644
--- a/orc11/value.v
+++ b/gpfsl/orc11/value.v
@@ -1,4 +1,4 @@
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Require Import stdpp.options.
 
diff --git a/orc11/view.v b/gpfsl/orc11/view.v
similarity index 99%
rename from orc11/view.v
rename to gpfsl/orc11/view.v
index 215c8b5ad29245c8881b8087f9f1975bfba46b8b..d8259f6a86e0960fc823705957971b8f0b5fac0a 100644
--- a/orc11/view.v
+++ b/gpfsl/orc11/view.v
@@ -1,4 +1,4 @@
-From orc11 Require Export location.
+From gpfsl.orc11 Require Export location.
 
 Require Import stdpp.options.