From c59e1f8583ab8224023003a1ba3bc6407c82de94 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Feb 2016 12:41:56 +0100
Subject: [PATCH] More solve_propers.

---
 program_logic/auth.v            | 2 +-
 program_logic/ghost_ownership.v | 2 +-
 program_logic/hoare.v           | 4 ++--
 program_logic/ownership.v       | 2 +-
 program_logic/viewshifts.v      | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/program_logic/auth.v b/program_logic/auth.v
index 3cb74b808..362e3e4fe 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -42,7 +42,7 @@ Section auth.
   Global Instance auth_own_ne n γ : Proper (dist n ==> dist n) (auth_own γ).
   Proof. rewrite auth_own_eq; solve_proper. Qed.
   Global Instance auth_own_proper γ : Proper ((≡) ==> (≡)) (auth_own γ).
-  Proof. by rewrite auth_own_eq /auth_own_def=> a b ->. Qed.
+  Proof. by rewrite auth_own_eq; solve_proper. Qed.
   Global Instance auth_own_timeless γ a : TimelessP (auth_own γ a).
   Proof. rewrite auth_own_eq. apply _. Qed.
 
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 9e580abf9..ad194c529 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -64,7 +64,7 @@ Qed.
 
 (** * Properties of own *)
 Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
-Proof. by intros m m' Hm; rewrite /own Hm. Qed.
+Proof. solve_proper. Qed.
 Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own γ) := ne_proper _.
 
 Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ≡ (own γ a1 ★ own γ a2)%I.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index e9bf2d02f..95992a776 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -30,13 +30,13 @@ Global Instance ht_ne E n :
 Proof. solve_proper. Qed.
 Global Instance ht_proper E :
   Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Λ Σ E).
-Proof. by intros P P' HP e ? <- Φ Φ' HΦ; rewrite /ht HP; setoid_rewrite HΦ. Qed.
+Proof. solve_proper. Qed.
 Lemma ht_mono E P P' Φ Φ' e :
   P ⊑ P' → (∀ v, Φ' v ⊑ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊑ {{ P }} e @ E {{ Φ }}.
 Proof. by intros; apply always_mono, impl_mono, wp_mono. Qed.
 Global Instance ht_mono' E :
   Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Λ Σ E).
-Proof. by intros P P' HP e ? <- Φ Φ' HΦ; apply ht_mono. Qed.
+Proof. solve_proper. Qed.
 
 Lemma ht_alt E P Φ e : (P ⊑ || e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
 Proof.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 4b2c543bb..4b657f72b 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -46,7 +46,7 @@ Proof. rewrite /ownP; apply _. Qed.
 
 (* ghost state *)
 Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
-Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
+Proof. solve_proper. Qed.
 Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Λ Σ) := ne_proper _.
 Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
 Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 014e0bdb9..a01eab178 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -41,7 +41,7 @@ Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
 
 Global Instance vs_mono' E1 E2 :
   Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Λ Σ E1 E2).
-Proof. by intros until 2; apply vs_mono. Qed.
+Proof. solve_proper. Qed.
 
 Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
 Proof. apply vs_alt, False_elim. Qed.
-- 
GitLab