Commit 9dbd5aee authored by Janno's avatar Janno

Shorten type annotations a bit.

parent 13c1d3dc
......@@ -598,11 +598,12 @@ Fixpoint first {A} (ls: mlist (TT.ttac A)) : TT.ttac A :=
| mnil => mfail "No applicable tactic."
end.
Definition wp_store : tactic :=
iStartProof $ iStartHeapProof "wp_store" $ λ '(IHeapGoal Σ _ Δ s e E Φ),
(reshape_expr_wp e $ λ K e',
' Δ'' v v' i l e'' <- M.evar _;
TT.change_dep (λ e, envs_entails _ (WP e @ _ ; _ {{ _ }})) _ (
TT.change_dep (λ e, _ (WP e @ _ ; _ {{ _ }})) _ (
TT.apply (tac_wp_store Δ Δ' Δ'' s E i K l v e'' v' Φ)
<**> TT.apply_ (* IntoVal *)
<**> TT.apply_ (* IntoLaterEnvs *)
......@@ -611,7 +612,7 @@ Definition wp_store : tactic :=
<**> `e' <- M.evar _;
wp_expr_simpl_subst e'
<**> first [m: `e'' <- M.evar _;
TT.change_dep (fun e => envs_entails _ (wp _ _ e _)) e' (wp_pure (Seq (Lit LitUnit) e''))
TT.change_dep (fun e => _ WP e @ _ ; _ {{ _ }}) e' (wp_pure (Seq (Lit LitUnit) e''))
| TT.try wp_value_head]
) ||[TT.TTchange_Exception] raise TryNextDecomposition
) ||[ReshapeExprExc] mfail "wp_store: cannot find 'Store' in " e.
......
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