Commit 111c0332 authored by Ralf Jung's avatar Ralf Jung
Browse files

use new select tactic from std++

parent 858665ff
......@@ -248,7 +248,7 @@ Proof.
- by destruct 1; simpl; intros ?; setoid_subst.
- by intros ? [|]; destruct 1; inversion_clear 1; econstructor; setoid_subst.
- destruct 3; simpl in *; destruct_and?; eauto using closed_op;
match goal with H : closed _ _ |- _ => destruct H end; set_solver.
select (closed _ _) (fun H => destruct H); set_solver.
- intros []; naive_solver eauto using closed_up, closed_up_set,
elem_of_up, elem_of_up_set with sts.
- intros [] [] [] _ _ _ _ _; constructor; rewrite ?assoc; auto with sts.
......
......@@ -34,7 +34,7 @@ Section modalities.
(MIEnvFilter Objective) (MIEnvFilter Objective).
Proof.
split; simpl; split_and?; intros;
try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
try select (TCDiag _ _ _) (fun H => destruct H);
eauto using bi.equiv_entails_sym, objective_objectively,
monPred_objectively_mono, monPred_objectively_and,
monPred_objectively_sep_2 with typeclass_instances.
......
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