From 5e9a8aedd5700b9615f36896918d16755bc41bd9 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 20 Mar 2019 16:25:05 +0100
Subject: [PATCH] Remove unnecessary arguments from `ResolveProphS`.

---
 theories/heap_lang/lang.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index effcebd5f..3cf55913b 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -557,9 +557,7 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ)
                []
-  | ResolveProphS e1 p e2 v σ :
-     to_val e1 = Some (LitV $ LitProphecy p) →
-     to_val e2 = Some v →
+  | ResolveProphS p v σ :
      head_step (ResolveProph (Val $ LitV $ LitProphecy p) (Val v)) σ
                [(p, v)]
                (Val $ LitV LitUnit) σ [].
-- 
GitLab