diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 360dc4778c5cab280d9bb560556d69067fb45add..0392aaf6a8d7865765aa33f2a0b8a884e35e829c 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -306,24 +306,24 @@ Proof.
 Qed.
 
 Program Definition agreeRF (F : cFunctor) : rFunctor := {|
-  rFunctor_car A B := agreeR (cFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg)
+  rFunctor_car A _ B _ := agreeR (cFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  intros ? A1 A2 B1 B2 n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x; simpl. rewrite -{2}(agree_map_id x).
+  intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
   apply (agree_map_ext _)=>y. by rewrite cFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
   apply (agree_map_ext _)=>y; apply cFunctor_compose.
 Qed.
 
 Instance agreeRF_contractive F :
   cFunctorContractive F → rFunctorContractive (agreeRF F).
 Proof.
-  intros ? A1 A2 B1 B2 n ???; simpl.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
   by apply agreeC_map_ne, cFunctor_contractive.
 Qed.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 927eddaecb9c02f94fc89b49c7df5db59fa6a108..4af018de3c71ef4978c632f70f2f91e3de1f6169 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -403,13 +403,13 @@ Proof. destruct x as [[[]|] ]; by rewrite // /auth_map /= agree_map_id. Qed.
 Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
   auth_map (g ∘ f) x = auth_map g (auth_map f x).
 Proof. destruct x as [[[]|] ];  by rewrite // /auth_map /= agree_map_compose. Qed.
-Lemma auth_map_ext {A B : ofeT} (f g : A → B) `{_ : NonExpansive f} x :
+Lemma auth_map_ext {A B : ofeT} (f g : A → B) `{!NonExpansive f} x :
   (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
 Proof.
   constructor; simpl; auto.
   apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
 Qed.
-Instance auth_map_ne {A B : ofeT} (f : A -> B) {Hf : NonExpansive f} :
+Instance auth_map_ne {A B : ofeT} (f : A -> B) `{Hf : !NonExpansive f} :
   NonExpansive (auth_map f).
 Proof.
   intros n [??] [??] [??]; split; simpl in *; [|by apply Hf].
@@ -437,45 +437,45 @@ Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
   apply agreeC_map_ne; auto. Qed.
 
 Program Definition authRF (F : urFunctor) : rFunctor := {|
-  rFunctor_car A B := authR (urFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
+  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authC_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y. apply _. apply urFunctor_id.
+  intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
+  apply (auth_map_ext _ _)=>y; apply urFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y. apply _. apply urFunctor_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_compose.
 Qed.
 
 Instance authRF_contractive F :
   urFunctorContractive F → rFunctorContractive (authRF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_contractive.
 Qed.
 
 Program Definition authURF (F : urFunctor) : urFunctor := {|
-  urFunctor_car A B := authUR (urFunctor_car F A B);
-  urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
+  urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authC_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y. apply _. apply urFunctor_id.
+  intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
+  apply (auth_map_ext _ _)=>y; apply urFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y. apply _. apply urFunctor_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_compose.
 Qed.
 
 Instance authURF_contractive F :
   urFunctorContractive F → urFunctorContractive (authURF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authC_map_ne, urFunctor_contractive.
 Qed.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index ed6254f0bee39fef95c92d7abce8d3738bc08965..f44e3f3c423cd7681048541f839c090117237e64 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -766,16 +766,18 @@ End cmra_morphism.
 
 (** Functors *)
 Record rFunctor := RFunctor {
-  rFunctor_car : ofeT → ofeT → cmraT;
-  rFunctor_map {A1 A2 B1 B2} :
+  rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmraT;
+  rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
-  rFunctor_ne A1 A2 B1 B2 :
-    NonExpansive (@rFunctor_map A1 A2 B1 B2);
-  rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
-  rFunctor_compose {A1 A2 A3 B1 B2 B3}
+  rFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+    NonExpansive (@rFunctor_map A1 _ A2 _ B1 _ B2 _);
+  rFunctor_id `{!Cofe A, !Cofe B} (x : rFunctor_car A B) :
+    rFunctor_map (cid,cid) x ≡ x;
+  rFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
-  rFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
+  rFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
+      (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CmraMorphism (rFunctor_map fg)
 }.
 Existing Instances rFunctor_ne rFunctor_mor.
@@ -785,13 +787,15 @@ Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
 
 Class rFunctorContractive (F : rFunctor) :=
-  rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
+  rFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+    Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
-Definition rFunctor_diag (F: rFunctor) (A: ofeT) : cmraT := rFunctor_car F A A.
+Definition rFunctor_diag (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
+  rFunctor_car F A A.
 Coercion rFunctor_diag : rFunctor >-> Funclass.
 
 Program Definition constRF (B : cmraT) : rFunctor :=
-  {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
+  {| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
 Coercion constRF : cmraT >-> rFunctor.
 
@@ -799,16 +803,18 @@ Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
 
 Record urFunctor := URFunctor {
-  urFunctor_car : ofeT → ofeT → ucmraT;
-  urFunctor_map {A1 A2 B1 B2} :
+  urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmraT;
+  urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
-  urFunctor_ne A1 A2 B1 B2 :
-    NonExpansive (@urFunctor_map A1 A2 B1 B2);
-  urFunctor_id {A B} (x : urFunctor_car A B) : urFunctor_map (cid,cid) x ≡ x;
-  urFunctor_compose {A1 A2 A3 B1 B2 B3}
+  urFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+    NonExpansive (@urFunctor_map A1 _ A2 _ B1 _ B2 _);
+  urFunctor_id `{!Cofe A, !Cofe B} (x : urFunctor_car A B) :
+    urFunctor_map (cid,cid) x ≡ x;
+  urFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
-  urFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
+  urFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
+      (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CmraMorphism (urFunctor_map fg)
 }.
 Existing Instances urFunctor_ne urFunctor_mor.
@@ -818,13 +824,15 @@ Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
 
 Class urFunctorContractive (F : urFunctor) :=
-  urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
+  urFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+    Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
-Definition urFunctor_diag (F: urFunctor) (A: ofeT) : ucmraT := urFunctor_car F A A.
+Definition urFunctor_diag (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
+  urFunctor_car F A A.
 Coercion urFunctor_diag : urFunctor >-> Funclass.
 
 Program Definition constURF (B : ucmraT) : urFunctor :=
-  {| urFunctor_car A1 A2 := B; urFunctor_map A1 A2 B1 B2 f := cid |}.
+  {| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
 Coercion constURF : ucmraT >-> urFunctor.
 
@@ -1189,16 +1197,16 @@ Proof.
 Qed.
 
 Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
-  rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
-  rFunctor_map A1 A2 B1 B2 fg :=
+  rFunctor_car A _ B _ := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
     prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 A2 B1 B2 n ???. by apply prodC_map_ne; apply rFunctor_ne.
+  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodC_map_ne; apply rFunctor_ne.
 Qed.
-Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_id. Qed.
 Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
+  intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
   by rewrite !rFunctor_compose.
 Qed.
 Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
@@ -1207,21 +1215,21 @@ Instance prodRF_contractive F1 F2 :
   rFunctorContractive F1 → rFunctorContractive F2 →
   rFunctorContractive (prodRF F1 F2).
 Proof.
-  intros ?? A1 A2 B1 B2 n ???;
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
     by apply prodC_map_ne; apply rFunctor_contractive.
 Qed.
 
 Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
-  urFunctor_car A B := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
-  urFunctor_map A1 A2 B1 B2 fg :=
+  urFunctor_car A _ B _ := prodUR (urFunctor_car F1 A B) (urFunctor_car F2 A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
     prodC_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 A2 B1 B2 n ???. by apply prodC_map_ne; apply urFunctor_ne.
+  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodC_map_ne; apply urFunctor_ne.
 Qed.
-Next Obligation. by intros F1 F2 A B [??]; rewrite /= !urFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_id. Qed.
 Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
+  intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
   by rewrite !urFunctor_compose.
 Qed.
 Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
@@ -1230,7 +1238,7 @@ Instance prodURF_contractive F1 F2 :
   urFunctorContractive F1 → urFunctorContractive F2 →
   urFunctorContractive (prodURF F1 F2).
 Proof.
-  intros ?? A1 A2 B1 B2 n ???;
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
     by apply prodC_map_ne; apply urFunctor_contractive.
 Qed.
 
@@ -1450,47 +1458,47 @@ Proof.
 Qed.
 
 Program Definition optionRF (F : rFunctor) : rFunctor := {|
-  rFunctor_car A B := optionR (rFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
+  rFunctor_car A _ B _ := optionR (rFunctor_car F A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
   apply option_fmap_equiv_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
   apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
 Qed.
 
 Instance optionRF_contractive F :
   rFunctorContractive F → rFunctorContractive (optionRF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
 Qed.
 
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
-  urFunctor_car A B := optionUR (rFunctor_car F A B);
-  urFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
+  urFunctor_car A _ B _ := optionUR (rFunctor_car F A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
   apply option_fmap_equiv_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
   apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
 Qed.
 
 Instance optionURF_contractive F :
   rFunctorContractive F → urFunctorContractive (optionURF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
 Qed.
 
 (* Dependently-typed functions over a discrete domain *)
@@ -1573,23 +1581,23 @@ Proof.
 Qed.
 
 Program Definition ofe_funURF {C} (F : C → urFunctor) : urFunctor := {|
-  urFunctor_car A B := ofe_funUR (λ c, urFunctor_car (F c) A B);
-  urFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, urFunctor_map (F c) fg)
+  urFunctor_car A _ B _ := ofe_funUR (λ c, urFunctor_car (F c) A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := ofe_funC_map (λ c, urFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  intros C F A1 A2 B1 B2 n ?? g. by apply ofe_funC_map_ne=>?; apply urFunctor_ne.
+  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply ofe_funC_map_ne=>?; apply urFunctor_ne.
 Qed.
 Next Obligation.
-  intros C F A B g; simpl. rewrite -{2}(ofe_fun_map_id g).
+  intros C F A ? B ? g; simpl. rewrite -{2}(ofe_fun_map_id g).
   apply ofe_fun_map_ext=> y; apply urFunctor_id.
 Qed.
 Next Obligation.
-  intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-ofe_fun_map_compose.
+  intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-ofe_fun_map_compose.
   apply ofe_fun_map_ext=>y; apply urFunctor_compose.
 Qed.
 Instance ofe_funURF_contractive {C} (F : C → urFunctor) :
   (∀ c, urFunctorContractive (F c)) → urFunctorContractive (ofe_funURF F).
 Proof.
-  intros ? A1 A2 B1 B2 n ?? g.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
   by apply ofe_funC_map_ne=>c; apply urFunctor_contractive.
 Qed.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index b18a584e96f871943021fa1cac3b0bf847d91c89..33bfebd875ecf222ccbe703d9e653a0a78598f5c 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -4,8 +4,8 @@ Set Default Proof Using "Type".
 Record solution (F : cFunctor) := Solution {
   solution_car :> ofeT;
   solution_cofe : Cofe solution_car;
-  solution_unfold : solution_car -n> F solution_car;
-  solution_fold : F solution_car -n> solution_car;
+  solution_unfold : solution_car -n> F solution_car _;
+  solution_fold : F solution_car _ -n> solution_car;
   solution_fold_unfold X : solution_fold (solution_unfold X) ≡ X;
   solution_unfold_fold X : solution_unfold (solution_fold X) ≡ X
 }.
@@ -14,21 +14,25 @@ Arguments solution_fold {_} _.
 Existing Instance solution_cofe.
 
 Module solver. Section solver.
-Context (F : cFunctor) `{Fcontr : cFunctorContractive F}
-        `{Fcofe : ∀ T : ofeT, Cofe T → Cofe (F T)} `{Finh : Inhabited (F unitC)}.
+Context (F : cFunctor) `{Fcontr : cFunctorContractive F}.
+Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (F T _)}.
+Context `{Finh : Inhabited (F unitC _)}.
 Notation map := (cFunctor_map F).
 
-Fixpoint A (k : nat) : ofeT :=
-  match k with 0 => unitC | S k => F (A k) end.
-Local Instance: ∀ k, Cofe (A k).
-Proof using Fcofe. induction k; apply _. Defined.
+Fixpoint A' (k : nat) : { C : ofeT & Cofe C } :=
+  match k with
+  | 0 => existT (P:=Cofe) unitC _
+  | S k => existT (P:=Cofe) (F (projT1 (A' k)) (projT2 (A' k))) _
+  end.
+Notation A k := (projT1 (A' k)).
+Local Instance A_cofe k : Cofe (A k) := projT2 (A' k).
+
 Fixpoint f (k : nat) : A k -n> A (S k) :=
   match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
 with g (k : nat) : A (S k) -n> A k :=
   match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end.
 Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
 Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
-Arguments A : simpl never.
 Arguments f : simpl never.
 Arguments g : simpl never.
 
@@ -177,7 +181,7 @@ Proof.
   - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
 Qed.
 
-Program Definition unfold_chain (X : T) : chain (F T) :=
+Program Definition unfold_chain (X : T) : chain (F T _) :=
   {| chain_car n := map (project n,embed' n) (X (S n)) |}.
 Next Obligation.
   intros X n i Hi.
@@ -187,14 +191,14 @@ Next Obligation.
   rewrite f_S -cFunctor_compose.
   by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
-Definition unfold (X : T) : F T := compl (unfold_chain X).
+Definition unfold (X : T) : F T _ := compl (unfold_chain X).
 Instance unfold_ne : NonExpansive unfold.
 Proof.
   intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
     (conv_compl n (unfold_chain Y)) /= (HXY (S n)).
 Qed.
 
-Program Definition fold (X : F T) : T :=
+Program Definition fold (X : F T _) : T :=
   {| tower_car n := g n (map (embed' n,project n) X) |}.
 Next Obligation.
   intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index de491b25b91ecd6f606337adfe9549938c1b5654..805a9309b1a5947983981265e5939417d03f686e 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -100,7 +100,7 @@ Global Instance csum_ofe_discrete :
   OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumC.
 Proof. by inversion_clear 3; constructor; apply (discrete _). Qed.
 Global Instance csum_leibniz :
-  LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv (csumC A B).
+  LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv csumC.
 Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
 
 Global Instance Cinl_discrete a : Discrete a → Discrete (Cinl a).
@@ -367,18 +367,18 @@ Proof.
 Qed.
 
 Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
-  rFunctor_car A B := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
-  rFunctor_map A1 A2 B1 B2 fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
+  rFunctor_car A _ B _ := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
 |}.
 Next Obligation.
-  by intros Fa Fb A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
+  by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
 Qed.
 Next Obligation.
-  intros Fa Fb A B x. rewrite /= -{2}(csum_map_id x).
+  intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
   apply csum_map_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
-  intros Fa Fb A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -csum_map_compose.
+  intros Fa Fb A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -csum_map_compose.
   apply csum_map_ext=>y; apply rFunctor_compose.
 Qed.
 
@@ -386,5 +386,6 @@ Instance csumRF_contractive Fa Fb :
   rFunctorContractive Fa → rFunctorContractive Fb →
   rFunctorContractive (csumRF Fa Fb).
 Proof.
-  by intros ?? A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_contractive.
+  intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
+  by apply csumC_map_ne; try apply rFunctor_contractive.
 Qed.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 41956b4412f33d5ea92dbfae4e75186eb47bf569..8d99dec9ddeb8a90009c26a1c98958fca2813f52 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -150,23 +150,23 @@ Instance exclC_map_ne A B : NonExpansive (@exclC_map A B).
 Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
 
 Program Definition exclRF (F : cFunctor) : rFunctor := {|
-  rFunctor_car A B := (exclR (cFunctor_car F A B));
-  rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
+  rFunctor_car A _ B _ := (exclR (cFunctor_car F A B));
+  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
+  intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x; simpl. rewrite -{2}(excl_map_id x).
+  intros F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
   apply excl_map_ext=>y. by rewrite cFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -excl_map_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -excl_map_compose.
   apply excl_map_ext=>y; apply cFunctor_compose.
 Qed.
 
 Instance exclRF_contractive F :
   cFunctorContractive F → rFunctorContractive (exclRF F).
 Proof.
-  intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
+  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
 Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index f2bcdfe9919b9710933f370b339cd9c53da12f67..02df4be9695adb0e754b1416c847457b9d526ab2 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -558,43 +558,43 @@ Proof.
 Qed.
 
 Program Definition gmapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := gmapC K (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := gmapC_map (cFunctor_map F fg)
+  cFunctor_car A _ B _ := gmapC K (cFunctor_car F A B);
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
+  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
+  intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
   apply map_fmap_equiv_ext=>y ??; apply cFunctor_id.
 Qed.
 Next Obligation.
-  intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
+  intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
   apply map_fmap_equiv_ext=>y ??; apply cFunctor_compose.
 Qed.
 Instance gmapCF_contractive K `{Countable K} F :
   cFunctorContractive F → cFunctorContractive (gmapCF K F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
 Qed.
 
 Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
-  urFunctor_car A B := gmapUR K (rFunctor_car F A B);
-  urFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg)
+  urFunctor_car A _ B _ := gmapUR K (rFunctor_car F A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapC_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
+  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
 Qed.
 Next Obligation.
-  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
+  intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
   apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
 Qed.
 Next Obligation.
-  intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
+  intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
   apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
 Qed.
 Instance gmapRF_contractive K `{Countable K} F :
   rFunctorContractive F → urFunctorContractive (gmapURF K F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
 Qed.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index e15329c51e7c66e223c533af4c9df65778968647..c6d5a137cbeb79448097146b85be0dfe8942c7e3 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -113,25 +113,25 @@ Instance listC_map_ne A B : NonExpansive (@listC_map A B).
 Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
 
 Program Definition listCF (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := listC (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := listC_map (cFunctor_map F fg)
+  cFunctor_car A _ B _ := listC (cFunctor_car F A B);
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(list_fmap_id x).
+  intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
   apply list_fmap_equiv_ext=>y. apply cFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
   apply list_fmap_equiv_ext=>y; apply cFunctor_compose.
 Qed.
 
 Instance listCF_contractive F :
   cFunctorContractive F → cFunctorContractive (listCF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, cFunctor_contractive.
 Qed.
 
 (* CMRA *)
@@ -462,23 +462,23 @@ Proof.
 Qed.
 
 Program Definition listURF (F : urFunctor) : urFunctor := {|
-  urFunctor_car A B := listUR (urFunctor_car F A B);
-  urFunctor_map A1 A2 B1 B2 fg := listC_map (urFunctor_map F fg)
+  urFunctor_car A _ B _ := listUR (urFunctor_car F A B);
+  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listC_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F ???? n f g Hfg; apply listC_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, urFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(list_fmap_id x).
+  intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
   apply list_fmap_equiv_ext=>y. apply urFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
   apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
 Qed.
 
 Instance listURF_contractive F :
   urFunctorContractive F → urFunctorContractive (listURF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listC_map_ne, urFunctor_contractive.
 Qed.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 6db8d6e8054f453cc9a078f86ddb4b72e3998485..52bc4c554c43c52e7f998fe34772d916beda83dd 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -664,14 +664,14 @@ Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
 (** Functors *)
 Record cFunctor := CFunctor {
-  cFunctor_car : ofeT → ofeT → ofeT;
-  cFunctor_map {A1 A2 B1 B2} :
+  cFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofeT;
+  cFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
-  cFunctor_ne {A1 A2 B1 B2} :
-    NonExpansive (@cFunctor_map A1 A2 B1 B2);
-  cFunctor_id {A B : ofeT} (x : cFunctor_car A B) :
+  cFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+    NonExpansive (@cFunctor_map A1 _ A2 _ B1 _ B2 _);
+  cFunctor_id `{!Cofe A, !Cofe B} (x : cFunctor_car A B) :
     cFunctor_map (cid,cid) x ≡ x;
-  cFunctor_compose {A1 A2 A3 B1 B2 B3}
+  cFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x)
 }.
@@ -682,14 +682,19 @@ Delimit Scope cFunctor_scope with CF.
 Bind Scope cFunctor_scope with cFunctor.
 
 Class cFunctorContractive (F : cFunctor) :=
-  cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).
+  cFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+    Contractive (@cFunctor_map F A1 _ A2 _ B1 _ B2 _).
 Hint Mode cFunctorContractive ! : typeclass_instances.
 
-Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A.
+Definition cFunctor_diag (F: cFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
+  cFunctor_car F A A.
+(** Note that the implicit argument [Cofe A] is not taken into account when
+[cFunctor_diag] is used as a coercion. So, given [F : cFunctor] and [A : ofeT]
+one has to write [F A _]. *)
 Coercion cFunctor_diag : cFunctor >-> Funclass.
 
 Program Definition constCF (B : ofeT) : cFunctor :=
-  {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
+  {| cFunctor_car A1 A2 _ _ := B; cFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
 Solve Obligations with done.
 Coercion constCF : ofeT >-> cFunctor.
 
@@ -697,21 +702,21 @@ Instance constCF_contractive B : cFunctorContractive (constCF B).
 Proof. rewrite /cFunctorContractive; apply _. Qed.
 
 Program Definition idCF : cFunctor :=
-  {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
+  {| cFunctor_car A1 _ A2 _ := A2; cFunctor_map A1 _ A2 _ B1 _ B2 _ f := f.2 |}.
 Solve Obligations with done.
 Notation "∙" := idCF : cFunctor_scope.
 
 Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
-  cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
-  cFunctor_map A1 A2 B1 B2 fg :=
+  cFunctor_car A _ B _ := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
     prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne.
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodC_map_ne; apply cFunctor_ne.
 Qed.
-Next Obligation. by intros F1 F2 A B [??]; rewrite /= !cFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !cFunctor_id. Qed.
 Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
+  intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
   by rewrite !cFunctor_compose.
 Qed.
 Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
@@ -720,25 +725,25 @@ Instance prodCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
   cFunctorContractive (prodCF F1 F2).
 Proof.
-  intros ?? A1 A2 B1 B2 n ???;
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
     by apply prodC_map_ne; apply cFunctor_contractive.
 Qed.
 
 Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
-  cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
-  cFunctor_map A1 A2 B1 B2 fg :=
+  cFunctor_car A _ B _ := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
     ofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
+  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
   apply ofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
 Qed.
 Next Obligation.
-  intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
+  intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !cFunctor_id.
   apply (ne_proper f). apply cFunctor_id.
 Qed.
 Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [h ?] ?; simpl in *.
+  intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [h ?] ?; simpl in *.
   rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose.
 Qed.
 Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
@@ -747,7 +752,7 @@ Instance ofe_morCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
   cFunctorContractive (ofe_morCF F1 F2).
 Proof.
-  intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
+  intros ?? A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
   apply ofe_morC_map_ne; apply cFunctor_contractive; destruct n, Hfg; by split.
 Qed.
 
@@ -818,16 +823,16 @@ Instance sumC_map_ne {A A' B B'} :
 Proof. intros n f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed.
 
 Program Definition sumCF (F1 F2 : cFunctor) : cFunctor := {|
-  cFunctor_car A B := sumC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
-  cFunctor_map A1 A2 B1 B2 fg :=
+  cFunctor_car A _ B _ := sumC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
     sumC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros ?? A1 A2 B1 B2 n ???; by apply sumC_map_ne; apply cFunctor_ne.
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumC_map_ne; apply cFunctor_ne.
 Qed.
-Next Obligation. by intros F1 F2 A B [?|?]; rewrite /= !cFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !cFunctor_id. Qed.
 Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [?|?]; simpl;
+  intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [?|?]; simpl;
     by rewrite !cFunctor_compose.
 Qed.
 Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
@@ -836,7 +841,7 @@ Instance sumCF_contractive F1 F2 :
   cFunctorContractive F1 → cFunctorContractive F2 →
   cFunctorContractive (sumCF F1 F2).
 Proof.
-  intros ?? A1 A2 B1 B2 n ???;
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
     by apply sumC_map_ne; apply cFunctor_contractive.
 Qed.
 
@@ -973,25 +978,25 @@ Instance optionC_map_ne A B : NonExpansive (@optionC_map A B).
 Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
 
 Program Definition optionCF (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := optionC (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg)
+  cFunctor_car A _ B _ := optionC (cFunctor_car F A B);
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
   apply option_fmap_equiv_ext=>y; apply cFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
   apply option_fmap_equiv_ext=>y; apply cFunctor_compose.
 Qed.
 
 Instance optionCF_contractive F :
   cFunctorContractive F → cFunctorContractive (optionCF F).
 Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
 Qed.
 
 (** Later *)
@@ -1075,26 +1080,26 @@ Instance laterC_map_contractive (A B : ofeT) : Contractive (@laterC_map A B).
 Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
 
 Program Definition laterCF (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := laterC (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := laterC_map (cFunctor_map F fg)
+  cFunctor_car A _ B _ := laterC (cFunctor_car F A B);
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := laterC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 A2 B1 B2 n fg fg' ?.
+  intros F A1 ? A2 ? B1 ? B2 ? n fg fg' ?.
   by apply (contractive_ne laterC_map), cFunctor_ne.
 Qed.
 Next Obligation.
-  intros F A B x; simpl. rewrite -{2}(later_map_id x).
+  intros F A ? B ? x; simpl. rewrite -{2}(later_map_id x).
   apply later_map_ext=>y. by rewrite cFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -later_map_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -later_map_compose.
   apply later_map_ext=>y; apply cFunctor_compose.
 Qed.
 Notation "â–¶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
 
 Instance laterCF_contractive F : cFunctorContractive (laterCF F).
 Proof.
-  intros A1 A2 B1 B2 n fg fg' Hfg. apply laterC_map_contractive.
+  intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterC_map_contractive.
   destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
 Qed.
 
@@ -1174,18 +1179,19 @@ Instance ofe_funC_map_ne {A} {B1 B2 : A → ofeT} :
 Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
 
 Program Definition ofe_funCF {C} (F : C → cFunctor) : cFunctor := {|
-  cFunctor_car A B := ofe_funC (λ c, cFunctor_car (F c) A B);
-  cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, cFunctor_map (F c) fg)
+  cFunctor_car A _ B _ := ofe_funC (λ c, cFunctor_car (F c) A B);
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := ofe_funC_map (λ c, cFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  intros C F A1 A2 B1 B2 n ?? g. by apply ofe_funC_map_ne=>?; apply cFunctor_ne.
+  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply ofe_funC_map_ne=>?; apply cFunctor_ne.
 Qed.
 Next Obligation.
-  intros C F A B g; simpl. rewrite -{2}(ofe_fun_map_id g).
+  intros C F A ? B ? g; simpl. rewrite -{2}(ofe_fun_map_id g).
   apply ofe_fun_map_ext=> y; apply cFunctor_id.
 Qed.
 Next Obligation.
-  intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -ofe_fun_map_compose.
+  intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g.
+  rewrite /= -ofe_fun_map_compose.
   apply ofe_fun_map_ext=>y; apply cFunctor_compose.
 Qed.
 
@@ -1194,7 +1200,7 @@ Notation "T -c> F" := (@ofe_funCF T%type (λ _, F%CF)) : cFunctor_scope.
 Instance ofe_funCF_contractive {C} (F : C → cFunctor) :
   (∀ c, cFunctorContractive (F c)) → cFunctorContractive (ofe_funCF F).
 Proof.
-  intros ? A1 A2 B1 B2 n ?? g.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
   by apply ofe_funC_map_ne=>c; apply cFunctor_contractive.
 Qed.
 
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index 7250ce400546401f18b69a2a24d32c92b87d0401..f8d073ba13ea447141006d1fffc88308673ca7df 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -88,26 +88,26 @@ Instance vecC_map_ne {A A'} m :
 Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed.
 
 Program Definition vecCF (F : cFunctor) m : cFunctor := {|
-  cFunctor_car A B := vecC (cFunctor_car F A B) m;
-  cFunctor_map A1 A2 B1 B2 fg := vecC_map m (cFunctor_map F fg)
+  cFunctor_car A _ B _ := vecC (cFunctor_car F A B) m;
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := vecC_map m (cFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 A2 B1 B2 n m f g Hfg. by apply vecC_map_ne, cFunctor_ne.
+  intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecC_map_ne, cFunctor_ne.
 Qed.
 Next Obligation.
-  intros F m A B l.
+  intros F m A ? B ? l.
   change (vec_to_list (vec_map m (cFunctor_map F (cid, cid)) l) ≡ l).
   rewrite vec_to_list_map. apply listCF.
 Qed.
 Next Obligation.
-  intros F m A1 A2 A3 B1 B2 B3 f g f' g' l.
+  intros F m A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' l.
   change (vec_to_list (vec_map m (cFunctor_map F (f â—Ž g, g' â—Ž f')) l)
     ≡ vec_map m (cFunctor_map F (g, g')) (vec_map m (cFunctor_map F (f, f')) l)).
-  rewrite !vec_to_list_map. by apply (cFunctor_compose (listCF F)  f g f' g').
+  rewrite !vec_to_list_map. by apply: (cFunctor_compose (listCF F) f g f' g').
 Qed.
 
 Instance vecCF_contractive F m :
   cFunctorContractive F → cFunctorContractive (vecCF F m).
 Proof.
-  by intros ?? A1 A2 B1 B2 n ???; apply vecC_map_ne; first apply cFunctor_contractive.
+  by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecC_map_ne; first apply cFunctor_contractive.
 Qed.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 42b53f898bb257242879138deb3ccceeaa2cfc50..34945d66892760632936bbb4ffa197d9d5b2d61a 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -117,13 +117,14 @@ the construction, this way we are sure we do not use any properties of the
 construction, and also avoid Coq from blindly unfolding it. *)
 Module Type iProp_solution_sig.
   Parameter iPreProp : gFunctors → ofeT.
+  Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ).
+
   Definition iResUR (Σ : gFunctors) : ucmraT :=
-    ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
+    ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
   Notation iProp Σ := (uPredC (iResUR Σ)).
   Notation iPropI Σ := (uPredI (iResUR Σ)).
   Notation iPropSI Σ := (uPredSI (iResUR Σ)).
 
-  Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ).
   Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
   Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iProp Σ.
   Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
@@ -136,13 +137,13 @@ Module Export iProp_solution : iProp_solution_sig.
   Import cofe_solver.
   Definition iProp_result (Σ : gFunctors) :
     solution (uPredCF (iResF Σ)) := solver.result _.
-
   Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ.
+  Global Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ) := _.
+
   Definition iResUR (Σ : gFunctors) : ucmraT :=
-    ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
+    ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
   Notation iProp Σ := (uPredC (iResUR Σ)).
 
-  Global Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ) := _.
   Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
     solution_fold (iProp_result Σ).
   Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index d3475828577f3c2f2050415a2a2530f8b380be35..4540dc68f1946e536437665cd3a7abc37b768590 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -10,10 +10,10 @@ individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
 needed because Coq is otherwise unable to solve type class constraints due to
 higher-order unification problems. *)
 Class inG (Σ : gFunctors) (A : cmraT) :=
-  InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) }.
+  InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) _ }.
 Arguments inG_id {_ _} _.
 
-Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (F (iPreProp Σ)).
+Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (F (iPreProp Σ) _).
 Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
 
 (** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 7e3401fd330e7371cf50a4eef8de2a06c3dd7e2d..f844bcc0bb63f6d6e8c150f87a74ab2ad95c6bd2 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -9,7 +9,7 @@ Import uPred.
    saved whatever-you-like. *)
 
 Class savedAnythingG (Σ : gFunctors) (F : cFunctor) := SavedAnythingG {
-  saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ)));
+  saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ) _));
   saved_anything_contractive : cFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
 }.
 Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
@@ -20,14 +20,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
 Proof. solve_inG. Qed.
 
 Definition saved_anything_own `{!savedAnythingG Σ F}
-    (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
+    (γ : gname) (x : F (iProp Σ) _) : iProp Σ :=
   own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_anything_own.
 Instance: Params (@saved_anything_own) 4 := {}.
 
 Section saved_anything.
   Context `{!savedAnythingG Σ F}.
-  Implicit Types x y : F (iProp Σ).
+  Implicit Types x y : F (iProp Σ) _.
   Implicit Types γ : gname.
 
   Global Instance saved_anything_persistent γ x :
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b9c90e9708a24cc6dca41d2c45f6a5786ffde16a..df7df317133753818dcaf439eb01f4d8fd17d04e 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -161,26 +161,26 @@ Proof.
 Qed.
 
 Program Definition uPredCF (F : urFunctor) : cFunctor := {|
-  cFunctor_car A B := uPredC (urFunctor_car F B A);
-  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
+  cFunctor_car A _ B _ := uPredC (urFunctor_car F B A);
+  cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
 |}.
 Next Obligation.
-  intros F A1 A2 B1 B2 n P Q HPQ.
+  intros F A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
   apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
 Qed.
 Next Obligation.
-  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
+  intros F A ? B ? P; simpl. rewrite -{2}(uPred_map_id P).
   apply uPred_map_ext=>y. by rewrite urFunctor_id.
 Qed.
 Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
+  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' P; simpl. rewrite -uPred_map_compose.
   apply uPred_map_ext=>y; apply urFunctor_compose.
 Qed.
 
 Instance uPredCF_contractive F :
   urFunctorContractive F → cFunctorContractive (uPredCF F).
 Proof.
-  intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive.
+  intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive.
   destruct n; split; by apply HPQ.
 Qed.