From 648260de8a3d6d2c067d9b4f6fd6a7142994b32d Mon Sep 17 00:00:00 2001 From: Gaurav Parthasarathy <gauravp@student.ethz.ch> Date: Wed, 3 Jul 2019 14:43:46 +0200 Subject: [PATCH] small fix in code description --- theories/logatom/rdcss/rdcss.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v index 0e9002b5..93ddbc5f 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 := -- GitLab