diff --git a/_CoqProject b/_CoqProject
index 43f1f574e191bce8bdc0a8612450ff8f8358e5d6..cbdb539dea7f671e5b7b3235081a59bc146c4704 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -17,6 +17,7 @@ theories/examples/sort_br_del.v
 theories/examples/sort_fg.v
 theories/examples/map.v
 theories/examples/map_reduce.v
+theories/examples/subprotocols.v
 theories/logrel/model.v
 theories/logrel/kind_tele.v
 theories/logrel/subtyping.v
diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index 0295aff9e2748a776fda95329c57a49dc061dd17..4b91685ee25fbd118b5d03d5c3fadfc7545a8886 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -9,4 +9,4 @@ Section basics.
     (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END)%proto.
   Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame "Hl1 Hl2'". Qed.
 
-End pair.
+End basics.