diff --git a/README.md b/README.md
index 490eb4597e80052d208d94f59117507d15668f4c..6cb88b2a127a0e984d940f7b3b65070530c3cc51 100644
--- a/README.md
+++ b/README.md
@@ -165,7 +165,7 @@ verification of programs written that language.
 
 * An example verification of the Message-Passing example, which has stronger
   resource reclamation than both examples given in Figure 4 of the RBrlx paper,
-  is given in [examples/mp_reclaim.v](gpfsl/examples/mp_reclaim.v)
+  is given in [examples/mp_reclaim.v](gpfsl-examples/mp_reclaim.v)
 
 [Iris]: https://gitlab.mpi-sws.org/iris/iris
 [iGPS]: http://plv.mpi-sws.org/igps/
diff --git a/_CoqProject b/_CoqProject
index 81a08e00f5e2a9426e0d53353eb458c62875999e..e11caadd2f65c65357af70488fc90dd90b0366f1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,7 +1,8 @@
 # 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 gpfsl gpfsl
 -Q orc11 orc11
+-Q gpfsl gpfsl
+-Q gpfsl-examples gpfsl.examples
 # silence coq_makefile warning
 -docroot gpfsl
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
@@ -106,33 +107,33 @@ gpfsl/gps/surface_iPP.v
 gpfsl/gps/surface.v
 
 # Examples
-gpfsl/examples/uniq_token.v
-gpfsl/examples/nat_tokens.v
-gpfsl/examples/map_seq.v
+gpfsl-examples/uniq_token.v
+gpfsl-examples/nat_tokens.v
+gpfsl-examples/map_seq.v
 
 ## Message-Passing
-gpfsl/examples/mp/code.v
-gpfsl/examples/mp/spec.v
-gpfsl/examples/mp/proof_gps.v
-gpfsl/examples/mp/proof_reclaim_gps.v
-gpfsl/examples/mp/proof_gen_inv.v
+gpfsl-examples/mp/code.v
+gpfsl-examples/mp/spec.v
+gpfsl-examples/mp/proof_gps.v
+gpfsl-examples/mp/proof_reclaim_gps.v
+gpfsl-examples/mp/proof_gen_inv.v
 ## Locks
-gpfsl/examples/lock/code_ticket_lock.v
-gpfsl/examples/lock/proof_ticket_lock_gps.v
+gpfsl-examples/lock/code_ticket_lock.v
+gpfsl-examples/lock/proof_ticket_lock_gps.v
 ## Circular Buffer
-gpfsl/examples/circ_buff/code.v
-gpfsl/examples/circ_buff/code_na.v
-gpfsl/examples/circ_buff/proof_gps.v
+gpfsl-examples/circ_buff/code.v
+gpfsl-examples/circ_buff/code_na.v
+gpfsl-examples/circ_buff/proof_gps.v
 ## Stack
-gpfsl/examples/stack/spec_na.v
-gpfsl/examples/stack/spec_per_elem.v
-gpfsl/examples/stack/code_na.v
-gpfsl/examples/stack/proof_na.v
-gpfsl/examples/stack/code_treiber.v
-gpfsl/examples/stack/proof_treiber_gps.v
+gpfsl-examples/stack/spec_na.v
+gpfsl-examples/stack/spec_per_elem.v
+gpfsl-examples/stack/code_na.v
+gpfsl-examples/stack/proof_na.v
+gpfsl-examples/stack/code_treiber.v
+gpfsl-examples/stack/proof_treiber_gps.v
 ## Queue
-gpfsl/examples/queue/spec_per_elem.v
-gpfsl/examples/queue/code_ms.v
-gpfsl/examples/queue/proof_ms_gps.v
+gpfsl-examples/queue/spec_per_elem.v
+gpfsl-examples/queue/code_ms.v
+gpfsl-examples/queue/proof_ms_gps.v
 ## Chase-Lev Double-ended Queue
-gpfsl/examples/chase_lev/code.v
+gpfsl-examples/chase_lev/code.v
diff --git a/gpfsl/examples/chase_lev/code.v b/gpfsl-examples/chase_lev/code.v
similarity index 100%
rename from gpfsl/examples/chase_lev/code.v
rename to gpfsl-examples/chase_lev/code.v
diff --git a/gpfsl/examples/circ_buff/code.v b/gpfsl-examples/circ_buff/code.v
similarity index 100%
rename from gpfsl/examples/circ_buff/code.v
rename to gpfsl-examples/circ_buff/code.v
diff --git a/gpfsl/examples/circ_buff/code_na.v b/gpfsl-examples/circ_buff/code_na.v
similarity index 100%
rename from gpfsl/examples/circ_buff/code_na.v
rename to gpfsl-examples/circ_buff/code_na.v
diff --git a/gpfsl/examples/circ_buff/proof_gps.v b/gpfsl-examples/circ_buff/proof_gps.v
similarity index 100%
rename from gpfsl/examples/circ_buff/proof_gps.v
rename to gpfsl-examples/circ_buff/proof_gps.v
diff --git a/gpfsl/examples/lock/code_ticket_lock.v b/gpfsl-examples/lock/code_ticket_lock.v
similarity index 100%
rename from gpfsl/examples/lock/code_ticket_lock.v
rename to gpfsl-examples/lock/code_ticket_lock.v
diff --git a/gpfsl/examples/lock/proof_ticket_lock_gps.v b/gpfsl-examples/lock/proof_ticket_lock_gps.v
similarity index 100%
rename from gpfsl/examples/lock/proof_ticket_lock_gps.v
rename to gpfsl-examples/lock/proof_ticket_lock_gps.v
diff --git a/gpfsl/examples/map_seq.v b/gpfsl-examples/map_seq.v
similarity index 100%
rename from gpfsl/examples/map_seq.v
rename to gpfsl-examples/map_seq.v
diff --git a/gpfsl/examples/mp/code.v b/gpfsl-examples/mp/code.v
similarity index 100%
rename from gpfsl/examples/mp/code.v
rename to gpfsl-examples/mp/code.v
diff --git a/gpfsl/examples/mp/proof_gen_inv.v b/gpfsl-examples/mp/proof_gen_inv.v
similarity index 100%
rename from gpfsl/examples/mp/proof_gen_inv.v
rename to gpfsl-examples/mp/proof_gen_inv.v
diff --git a/gpfsl/examples/mp/proof_gps.v b/gpfsl-examples/mp/proof_gps.v
similarity index 100%
rename from gpfsl/examples/mp/proof_gps.v
rename to gpfsl-examples/mp/proof_gps.v
diff --git a/gpfsl/examples/mp/proof_reclaim_gps.v b/gpfsl-examples/mp/proof_reclaim_gps.v
similarity index 100%
rename from gpfsl/examples/mp/proof_reclaim_gps.v
rename to gpfsl-examples/mp/proof_reclaim_gps.v
diff --git a/gpfsl/examples/mp/spec.v b/gpfsl-examples/mp/spec.v
similarity index 100%
rename from gpfsl/examples/mp/spec.v
rename to gpfsl-examples/mp/spec.v
diff --git a/gpfsl/examples/nat_tokens.v b/gpfsl-examples/nat_tokens.v
similarity index 100%
rename from gpfsl/examples/nat_tokens.v
rename to gpfsl-examples/nat_tokens.v
diff --git a/gpfsl/examples/queue/code_ms.v b/gpfsl-examples/queue/code_ms.v
similarity index 100%
rename from gpfsl/examples/queue/code_ms.v
rename to gpfsl-examples/queue/code_ms.v
diff --git a/gpfsl/examples/queue/proof_ms_gps.v b/gpfsl-examples/queue/proof_ms_gps.v
similarity index 100%
rename from gpfsl/examples/queue/proof_ms_gps.v
rename to gpfsl-examples/queue/proof_ms_gps.v
diff --git a/gpfsl/examples/queue/spec_per_elem.v b/gpfsl-examples/queue/spec_per_elem.v
similarity index 100%
rename from gpfsl/examples/queue/spec_per_elem.v
rename to gpfsl-examples/queue/spec_per_elem.v
diff --git a/gpfsl/examples/stack/code_na.v b/gpfsl-examples/stack/code_na.v
similarity index 100%
rename from gpfsl/examples/stack/code_na.v
rename to gpfsl-examples/stack/code_na.v
diff --git a/gpfsl/examples/stack/code_treiber.v b/gpfsl-examples/stack/code_treiber.v
similarity index 100%
rename from gpfsl/examples/stack/code_treiber.v
rename to gpfsl-examples/stack/code_treiber.v
diff --git a/gpfsl/examples/stack/proof_na.v b/gpfsl-examples/stack/proof_na.v
similarity index 100%
rename from gpfsl/examples/stack/proof_na.v
rename to gpfsl-examples/stack/proof_na.v
diff --git a/gpfsl/examples/stack/proof_treiber_gps.v b/gpfsl-examples/stack/proof_treiber_gps.v
similarity index 100%
rename from gpfsl/examples/stack/proof_treiber_gps.v
rename to gpfsl-examples/stack/proof_treiber_gps.v
diff --git a/gpfsl/examples/stack/spec_na.v b/gpfsl-examples/stack/spec_na.v
similarity index 100%
rename from gpfsl/examples/stack/spec_na.v
rename to gpfsl-examples/stack/spec_na.v
diff --git a/gpfsl/examples/stack/spec_per_elem.v b/gpfsl-examples/stack/spec_per_elem.v
similarity index 100%
rename from gpfsl/examples/stack/spec_per_elem.v
rename to gpfsl-examples/stack/spec_per_elem.v
diff --git a/gpfsl/examples/uniq_token.v b/gpfsl-examples/uniq_token.v
similarity index 100%
rename from gpfsl/examples/uniq_token.v
rename to gpfsl-examples/uniq_token.v