Commit eda63869 authored by Janno's avatar Janno

Prepare code for change to dep. goal type.

parent e146beea
...@@ -89,7 +89,7 @@ Definition wp_value_head {Σ} `{heapG Σ} {Δ} {s} ...@@ -89,7 +89,7 @@ Definition wp_value_head {Σ} `{heapG Σ} {Δ} {s}
{E : coPset} {e : language.expr heap_lang} {E : coPset} {e : language.expr heap_lang}
{Φ : language.val heap_lang iProp Σ} {Φ : language.val heap_lang iProp Σ}
: :
M ((envs_entails Δ (WP e @ s; E {{ v, Φ v }}))%I *m mlist goal) := M ((envs_entails Δ (WP e @ s; E {{ v, Φ v }}))%I *m mlist _) :=
e' <- evar _; e' <- evar _;
TT.apply (tac_wp_value Δ s E Φ e e') TT.apply (tac_wp_value Δ s E Φ e e')
<**> TT.apply_ <**> TT.apply_
......
...@@ -76,7 +76,7 @@ Definition iPropOf : iGoal -> Prop := fun '(IGoal M Δ P) => @envs_entails M Δ ...@@ -76,7 +76,7 @@ Definition iPropOf : iGoal -> Prop := fun '(IGoal M Δ P) => @envs_entails M Δ
Monomorphic Program Definition iStartProof (C : ig, TT.ttac (iPropOf ig)) : tactic := Monomorphic Program Definition iStartProof (C : ig, TT.ttac (iPropOf ig)) : tactic :=
(match_goal with (match_goal with
| [[? (G : Prop) |- G ]] => | [[? (G : Prop) |- G ]] =>
mmatch G in Prop as G' return M (G' *m mlist goal) with mmatch G in Prop as G' return M (G' *m mlist _) with
| [#] @envs_entails | M Δ P =n> (C (IGoal M Δ P)) | [#] @envs_entails | M Δ P =n> (C (IGoal M Δ P))
| _ => | _ =>
`M P <- M.evar _; `M P <- M.evar _;
......
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