Commit 2a4b76f7 authored by Dan Frumin's avatar Dan Frumin

Get rid of the unnecessary necessity modality

In the interpretation of recursive types
parent 9b373cca
......@@ -353,7 +353,7 @@ Section masked.
iExists (FoldV v'); iFrame "Hj".
rewrite fixpoint_unfold /= -interp_subst.
iAlways; iExists (_, _); eauto.
iExists (_, _); eauto.
Lemma bin_log_related_unfold Γ e e' τ :
......@@ -105,7 +105,7 @@ Section logrel.
Program Definition interp_rec1
(interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww,
( vv, ww = (FoldV (vv.1), FoldV (vv.2)) interp (τi :: Δ) vv)%I.
( vv, ww = (FoldV (vv.1), FoldV (vv.2)) interp (τi :: Δ) vv)%I.
Solve Obligations with solve_proper.
Global Instance interp_rec1_contractive
......@@ -166,8 +166,7 @@ Section logrel.
PersistentP (interp E1 E2 τ Δ vv).
revert vv Δ; induction τ=> vv Δ; simpl; try apply _.
rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec1 /=.
by apply always_intro'.
rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec1 /=. eauto.
Global Instance interp_env_persistent Γ E1 E2 Δ vvs :
PersistentP (interp_env Γ E1 E2 Δ vvs) := _.
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