Add missing `Hint Mode` for `ghost_var` and `gset_bij`.

Also put the arguments of `gset_bijG` in the right order.

iris/base_logic/lib/ghost_var.v

@@ -10,7 +10,10 @@ From iris.prelude Require Import options.
 Class ghost_varG Σ (A : Type) := GhostVarG {
   ghost_var_inG :> inG Σ (frac_agreeR $ leibnizO A);
 }.
-Definition ghost_varΣ (A : Type) : gFunctors := #[ GFunctor (frac_agreeR $ leibnizO A) ].
+Global Hint Mode ghost_varG - ! : typeclass_instances.
+
+Definition ghost_varΣ (A : Type) : gFunctors :=
+  #[ GFunctor (frac_agreeR $ leibnizO A) ].
 
 Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
 Proof. solve_inG. Qed.
@@ -26,7 +29,7 @@ Local Ltac unseal := rewrite ?ghost_var_eq /ghost_var_def.
 
 Section lemmas.
   Context `{!ghost_varG Σ A}.
-  Implicit Types (a : A) (q : Qp).
+  Implicit Types (a b : A) (q : Qp).
 
   Global Instance ghost_var_timeless γ q a : Timeless (ghost_var γ q a).
   Proof. unseal. apply _. Qed.

iris/base_logic/lib/gset_bij.v

@@ -27,16 +27,17 @@ From iris.proofmode Require Import tactics.
 From iris.prelude Require Import options.
 
 (* The uCMRA we need. *)
-Class gset_bijG A B `{Countable A, Countable B} Σ :=
+Class gset_bijG Σ A B `{Countable A, Countable B} :=
   GsetBijG { gset_bijG_inG :> inG Σ (gset_bijR A B); }.
+Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
 
 Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
   #[ GFunctor (gset_bijR A B) ].
 Global Instance subG_gset_bijΣ `{Countable A, Countable B} Σ :
-  subG (gset_bijΣ A B) Σ → gset_bijG A B Σ.
+  subG (gset_bijΣ A B) Σ → gset_bijG Σ A B.
 Proof. solve_inG. Qed.
 
-Definition gset_bij_own_auth_def `{gset_bijG A B Σ} (γ : gname)
+Definition gset_bij_own_auth_def `{gset_bijG Σ A B} (γ : gname)
     (q : Qp) (L : gset (A * B)) : iProp Σ :=
   own γ (gset_bij_auth q L).
 Definition gset_bij_own_auth_aux : seal (@gset_bij_own_auth_def). Proof. by eexists. Qed.
@@ -45,7 +46,7 @@ Definition gset_bij_own_auth_eq :
   @gset_bij_own_auth = @gset_bij_own_auth_def := seal_eq gset_bij_own_auth_aux.
 Arguments gset_bij_own_auth {_ _ _ _ _ _ _ _}.
 
-Definition gset_bij_own_elem_def `{gset_bijG A B Σ} (γ : gname)
+Definition gset_bij_own_elem_def `{gset_bijG Σ A B} (γ : gname)
   (a : A) (b : B) : iProp Σ := own γ (gset_bij_elem a b).
 Definition gset_bij_own_elem_aux : seal (@gset_bij_own_elem_def). Proof. by eexists. Qed.
 Definition gset_bij_own_elem := unseal gset_bij_own_elem_aux.
@@ -54,7 +55,7 @@ Definition gset_bij_own_elem_eq :
 Arguments gset_bij_own_elem {_ _ _ _ _ _ _ _}.
 
 Section gset_bij.
-  Context `{gset_bijG A B Σ}.
+  Context `{gset_bijG Σ A B}.
   Implicit Types (L : gset (A * B)) (a : A) (b : B).
 
   Global Instance gset_bij_own_auth_timeless γ q L :