From 55d07b4f8d415499b7b9dbf5bfcd3854a1dbdad2 Mon Sep 17 00:00:00 2001
From: Gaurav Parthasarathy <gauravp@student.ethz.ch>
Date: Mon, 8 Jul 2019 19:46:51 +0200
Subject: [PATCH] made proph_extract_winner only consider the first value in
the list
---
theories/logatom/rdcss/rdcss.v | 1 -
1 file changed, 1 deletion(-)
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index fe90d7a..f7c195e 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -161,7 +161,6 @@ Section rdcss.
Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
match pvs with
| ((_, #true)%V, LitV (LitProphecy p)) :: _ => Some p
- | _ :: vs => proph_extract_winner vs
| _ => None
end.
--
GitLab