Commit 95b66417 authored by Ralf Jung's avatar Ralf Jung
Browse files

use FromAssumption false in tac_assumption_coq

parent 1b5e1bc6
......@@ -92,14 +92,14 @@ Qed.
Lemma tac_assumption_coq Δ P Q :
( P)
FromAssumption true P Q
FromAssumption false P Q
(if env_spatial_is_nil Δ then TCTrue
else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ)))
envs_entails Δ Q.
Proof.
rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
rewrite envs_entails_unseal -(left_id emp%I bi_sep (of_envs Δ)).
rewrite -bi.intuitionistically_emp HP HPQ.
rewrite HP HPQ.
destruct (env_spatial_is_nil _) eqn:?.
- by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
- destruct H; by rewrite sep_elim_l.
......
......@@ -288,7 +288,7 @@ Tactic Notation "iAssumptionCoq" :=
let Hass := fresh in
match goal with
| H : ?P |- envs_entails _ ?Q =>
pose proof (_ : FromAssumption true P Q) as Hass;
pose proof (_ : FromAssumption false P Q) as Hass;
notypeclasses refine (tac_assumption_coq _ P _ H _ _);
[exact Hass
|pm_reduce; iSolveTC ||
......
Supports Markdown
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