From 61ede57eb9f6db365b98e4647c179adaedcdba31 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 29 Aug 2020 15:25:49 +0200
Subject: [PATCH] more consistent named arguments

---
 theories/algebra/ofe.v               | 2 +-
 theories/base_logic/lib/gen_heap.v   | 2 +-
 theories/base_logic/lib/invariants.v | 2 +-
 theories/base_logic/lib/own.v        | 2 +-
 theories/proofmode/environments.v    | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index db535df5d..258e41ff5 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -316,7 +316,7 @@ Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
   `{!Contractive f} : A := compl (fixpoint_chain f).
 Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
 Definition fixpoint := fixpoint_aux.(unseal).
-Arguments fixpoint {A AC AiH} f {Hf} : rename.
+Arguments fixpoint {A _ _} f {_}.
 Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
 
 Section fixpoint.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index aea6c15e0..efe8eb9b2 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -124,7 +124,7 @@ Section definitions.
   Definition meta := meta_aux.(unseal).
   Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
 End definitions.
-Arguments meta {_ _ _ _ Σ _ _ _ _} l N x.
+Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
 Local Notation "l ↦{ q } v" := (mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index c95573a02..4ddbe6895 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -11,7 +11,7 @@ Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   □ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
 Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
 Definition inv := inv_aux.(unseal).
-Arguments inv {Σ i} : rename.
+Arguments inv {Σ _} N P.
 Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
 Instance: Params (@inv) 3 := {}.
 
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 79d83df86..ed77ef6f1 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -59,7 +59,7 @@ Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
   uPred_ownM (iRes_singleton γ a).
 Definition own_aux : seal (@own_def). Proof. by eexists. Qed.
 Definition own := own_aux.(unseal).
-Arguments own {Σ A i} : rename.
+Arguments own {Σ A _} γ a.
 Definition own_eq : @own = @own_def := own_aux.(seal_eq).
 Instance: Params (@own) 4 := {}.
 
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 1be6f6992..194e1ec6f 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -269,7 +269,7 @@ Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
 Definition envs_entails_eq :
   @envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
 Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
-Arguments envs_entails {PROP} Δ Q%I : rename.
+Arguments envs_entails {PROP} Δ Q%I.
 Instance: Params (@envs_entails) 1 := {}.
 
 Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
-- 
GitLab