Commit 9936cb12 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'resolve_proph_fix' into 'master'

Remove unnecessary arguments from `ResolveProphS`.

See merge request iris/iris!227
parents ac6dc97b 5e9a8aed
......@@ -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) σ [].
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment