diff --git a/_CoqProject b/_CoqProject
index 98b145e01d55ab2310da730b3ea5705a63ace06e..4489ccb2876733d2156d6e1c85882966758f62ea 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -60,4 +60,4 @@ multi_actris/channel/proto_model.v
 multi_actris/channel/proto.v
 multi_actris/channel/channel.v
 multi_actris/channel/proofmode.v
-multi_actris/channel/proto_consistency_examples.v
+multi_actris/examples/basics.v
diff --git a/multi_actris/channel/proofmode.v b/multi_actris/channel/proofmode.v
index cc8cc2069a9add94f1fce088fcd1fdfd4df7a34e..9e729edb685b26ceaddc77ab30ef8b4b30ba1619 100644
--- a/multi_actris/channel/proofmode.v
+++ b/multi_actris/channel/proofmode.v
@@ -11,7 +11,7 @@ From iris.algebra Require Import gmap.
 From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 From iris.heap_lang Require Export proofmode notation.
 From multi_actris.channel Require Import proto_model.
-From multi_actris Require Export channel.
+From multi_actris.channel Require Export channel.
 Set Default Proof Using "Type".
 
 (** * Tactics for proving contractiveness of protocols *)