Commit bc45284f authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/select' into 'master'

use new select tactic from std++

See merge request !438
parents 701b533c 111c0332
Pipeline #27967 passed with stage
in 19 minutes and 43 seconds
...@@ -248,7 +248,7 @@ Proof. ...@@ -248,7 +248,7 @@ Proof.
- by destruct 1; simpl; intros ?; setoid_subst. - by destruct 1; simpl; intros ?; setoid_subst.
- by intros ? [|]; destruct 1; inversion_clear 1; econstructor; setoid_subst. - by intros ? [|]; destruct 1; inversion_clear 1; econstructor; setoid_subst.
- destruct 3; simpl in *; destruct_and?; eauto using closed_op; - 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, - intros []; naive_solver eauto using closed_up, closed_up_set,
elem_of_up, elem_of_up_set with sts. elem_of_up, elem_of_up_set with sts.
- intros [] [] [] _ _ _ _ _; constructor; rewrite ?assoc; auto with sts. - intros [] [] [] _ _ _ _ _; constructor; rewrite ?assoc; auto with sts.
......
...@@ -34,7 +34,7 @@ Section modalities. ...@@ -34,7 +34,7 @@ Section modalities.
(MIEnvFilter Objective) (MIEnvFilter Objective). (MIEnvFilter Objective) (MIEnvFilter Objective).
Proof. Proof.
split; simpl; split_and?; intros; 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, eauto using bi.equiv_entails_sym, objective_objectively,
monPred_objectively_mono, monPred_objectively_and, monPred_objectively_mono, monPred_objectively_and,
monPred_objectively_sep_2 with typeclass_instances. 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