diff --git a/_CoqProject b/_CoqProject
index 4de595c58b5312cf83897421606bde48ebf14d3b..f07602d425cccb20016be3be87220dd8dcdf2737 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -45,11 +45,11 @@ theories/typing/fixpoint.v
 theories/typing/type_sum.v
 theories/typing/typing.v
 theories/typing/soundness.v
-theories/typing/tests/get_x.v
-theories/typing/tests/rebor.v
-theories/typing/tests/unbox.v
-theories/typing/tests/init_prod.v
-theories/typing/tests/option_as_mut.v
-theories/typing/tests/unwrap_or.v
-theories/typing/tests/lazy_lft.v
+theories/typing/examples/get_x.v
+theories/typing/examples/rebor.v
+theories/typing/examples/unbox.v
+theories/typing/examples/init_prod.v
+theories/typing/examples/option_as_mut.v
+theories/typing/examples/unwrap_or.v
+theories/typing/examples/lazy_lft.v
 theories/typing/unsafe/cell.v
diff --git a/theories/typing/tests/get_x.v b/theories/typing/examples/get_x.v
similarity index 100%
rename from theories/typing/tests/get_x.v
rename to theories/typing/examples/get_x.v
diff --git a/theories/typing/tests/init_prod.v b/theories/typing/examples/init_prod.v
similarity index 100%
rename from theories/typing/tests/init_prod.v
rename to theories/typing/examples/init_prod.v
diff --git a/theories/typing/tests/lazy_lft.v b/theories/typing/examples/lazy_lft.v
similarity index 100%
rename from theories/typing/tests/lazy_lft.v
rename to theories/typing/examples/lazy_lft.v
diff --git a/theories/typing/tests/option_as_mut.v b/theories/typing/examples/option_as_mut.v
similarity index 100%
rename from theories/typing/tests/option_as_mut.v
rename to theories/typing/examples/option_as_mut.v
diff --git a/theories/typing/tests/rebor.v b/theories/typing/examples/rebor.v
similarity index 100%
rename from theories/typing/tests/rebor.v
rename to theories/typing/examples/rebor.v
diff --git a/theories/typing/tests/unbox.v b/theories/typing/examples/unbox.v
similarity index 100%
rename from theories/typing/tests/unbox.v
rename to theories/typing/examples/unbox.v
diff --git a/theories/typing/tests/unwrap_or.v b/theories/typing/examples/unwrap_or.v
similarity index 100%
rename from theories/typing/tests/unwrap_or.v
rename to theories/typing/examples/unwrap_or.v