From 111c03327520a961b30005f1e94b58ba923fc7a5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 May 2020 09:53:20 +0200
Subject: [PATCH] use new select tactic from std++
---
theories/algebra/sts.v | 2 +-
theories/proofmode/monpred.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index e270d09ae..5b4c19f5f 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -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.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index eca1b6094..78bcee3fc 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -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.
--
GitLab