diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 0e9002b54428aa91b82b8e877456aefd510556c9..93ddbc5f57b518956e370dbbe940c223390aef9f 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -28,8 +28,8 @@ Set Default Proof Using "Type".
 *)
 
 (*
-  new_rdcss() :=
-    let l_n = ref ( ref(injL 0) ) in
+  new_rdcss(init_v) :=
+    let l_n = ref ( ref(injL init_v) ) in
     ref l_n
  *)
 Definition new_rdcss : val :=