From 280725d6402ef90a6905f40699074039fedc8a86 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 29 Aug 2020 14:04:47 +0200
Subject: [PATCH] name more arguments in Arguments

---
 theories/base_logic/lib/fancy_updates.v   | 2 +-
 theories/base_logic/lib/gen_heap.v        | 4 ++--
 theories/bi/lib/atomic.v                  | 2 +-
 theories/program_logic/total_weakestpre.v | 2 +-
 theories/program_logic/weakestpre.v       | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 3334e0bcf..32aea0268 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -11,7 +11,7 @@ Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ
   wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P).
 Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
 Definition uPred_fupd := uPred_fupd_aux.(unseal).
-Arguments uPred_fupd {_ _}.
+Arguments uPred_fupd {Σ _}.
 Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
 Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
 
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 2014cd67d..aea6c15e0 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -75,8 +75,8 @@ Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
   gen_heap_name : gname;
   gen_meta_name : gname
 }.
-Arguments gen_heap_name {_ _ _ _ _} _ : assert.
-Arguments gen_meta_name {_ _ _ _ _} _ : assert.
+Arguments gen_heap_name {L V Σ _ _} _ : assert.
+Arguments gen_meta_name {L V Σ _ _} _ : assert.
 
 Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
   gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 817e5473b..bea7c6639 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -89,7 +89,7 @@ End definition.
 (** Seal it *)
 Definition atomic_update_aux : seal (@atomic_update_def). Proof. by eexists. Qed.
 Definition atomic_update := atomic_update_aux.(unseal).
-Arguments atomic_update {_ _ _ _}.
+Arguments atomic_update {PROP _ TA TB}.
 Definition atomic_update_eq : @atomic_update = _ := atomic_update_aux.(seal_eq).
 
 Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 380ef4f3c..dbba9257b 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -61,7 +61,7 @@ Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
   := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
 Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).
-Arguments twp' {_ _ _}.
+Arguments twp' {Λ Σ _}.
 Existing Instance twp'.
 Definition twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
 Proof. rewrite -twp_aux.(seal_eq) //. Qed.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 916f502f1..44f06bd7c 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -48,7 +48,7 @@ Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
   λ s : stuckness, fixpoint (wp_pre s).
 Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
 Definition wp' := wp_aux.(unseal).
-Arguments wp' {_ _ _}.
+Arguments wp' {Λ Σ _}.
 Existing Instance wp'.
 Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
 Proof. rewrite -wp_aux.(seal_eq) //. Qed.
-- 
GitLab