--- a/paper/cbc-type.tex	Mon Feb 06 15:42:45 2017 +0900
+++ b/paper/cbc-type.tex	Mon Feb 06 16:13:14 2017 +0900
@@ -222,7 +222,7 @@
 そしてノーマルレベルからアクセスできないよう分離した Meta Meta DataSegment である \verb/Meta/ にスタックの本体を格納する。
 CbC における実装では \verb/.../ で不定であった \verb/next/ も、agda ではメタレベルのコードセグメント \verb/nextCS/ となり、きちんと型付けされている。
 
-\lstinputlisting[label=agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda}
+\lstinputlisting[label=src:agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda}
 
 次にスタックへの操作に注目する。
 スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。
@@ -259,7 +259,7 @@
 
 \lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda}
 
-また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。 % TODO
+また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。
 
 % }}}