experiment

theories/lifetime/model/accessors.v

@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
 (** We want to keep these instances local, which means we have to repeat them in
 every model file that needs it. *)
 Local Existing Instance lftPreG_box.
-Local Hint Extern 10 (inG _ _) => solve_inG_with id lftΣ : typeclass_instances.
 
 Section accessors.
 Context `{!invG Σ, !lftG Σ}.

theories/lifetime/model/definitions.v

@@ -54,7 +54,16 @@ Notation lftPreG Σ := (subG lftΣ Σ).
 Local Instance lftPreG_box Σ : lftPreG Σ → boxG Σ.
 Proof. solve_inG. Qed.
 (** Instance for [own] *)
-Local Hint Extern 10 (inG _ _) => solve_inG_with id lftΣ : typeclass_instances.
+Instance lftPreG_1 Σ : lftPreG Σ → inG Σ (authR alftUR).
+Proof. solve_inG. Qed.
+Instance lftPreG_2 Σ : lftPreG Σ → inG Σ (authR ilftUR).
+Proof. solve_inG. Qed.
+Instance lftPreG_3 Σ : lftPreG Σ → inG Σ (authR borUR).
+Proof. solve_inG. Qed.
+Instance lftPreG_4 Σ : lftPreG Σ → inG Σ (authR natUR).
+Proof. solve_inG. Qed.
+Instance lftPreG_5 Σ : lftPreG Σ → inG Σ (authR inhUR).
+Proof. solve_inG. Qed.
 
 (** Library assumptions + instance names *)
 Class lftG Σ := LftG {

theories/lifetime/model/faking.v

@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
 (** We want to keep these instances local, which means we have to repeat them in
 every model file that needs it. *)
 Local Existing Instance lftPreG_box.
-Local Hint Extern 10 (inG _ _) => solve_inG_with id lftΣ : typeclass_instances.
 
 Section faking.
 Context `{!invG Σ, !lftG Σ}.

theories/lifetime/model/primitive.v

@@ -9,7 +9,6 @@ Import uPred.
 (** We want to keep these instances local, which means we have to repeat them in
 every model file that needs it. *)
 Local Existing Instance lftPreG_box.
-Local Hint Extern 10 (inG _ _) => solve_inG_with id lftΣ : typeclass_instances.
 
 Section primitive.
 Context `{!invG Σ, !lftG Σ}.

theories/lifetime/model/reborrow.v

@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
 (** We want to keep these instances local, which means we have to repeat them in
 every model file that needs it. *)
 Local Existing Instance lftPreG_box.
-Local Hint Extern 10 (inG _ _) => solve_inG_with id lftΣ : typeclass_instances.
 
 Section reborrow.
 Context `{!invG Σ, !lftG Σ}.