adapt to mc#19611

Author: Tragicus

theories/tvs.v

@@ -124,18 +124,16 @@ Definition entourage : set_system (E * E) :=
                      (forall xy : E * E,  (xy.1 - xy.2) \in U -> xy \in P).
 
 Let nbhs0N (U : set E) : nbhs (0 : E) U -> nbhs (0 : E) (-%R @` U).
-Proof. by apply: nbhs0N_subproof; exact: scale_continuous. Qed.
+Proof. by apply: (@nbhs0N_subproof _ _ (GRing.Lmodule.class E)); exact: scale_continuous. Qed.
 
 Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (-x) (-%R @` U).
-Proof.
-by apply: nbhsN_subproof; exact: scale_continuous.
-Qed.
+Proof. by apply: (@nbhsN_subproof _ _ (GRing.Lmodule.class E)); exact: scale_continuous. Qed.
 
 Let nbhsT (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U).
-Proof. by apply: nbhsT_subproof; exact: add_continuous. Qed.
+Proof. by apply: (@nbhsT_subproof _ _ (GRing.Lmodule.class E)); exact: add_continuous. Qed.
 
 Let nbhsB (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @`U).
-Proof. by apply: nbhsB_subproof; exact: add_continuous. Qed.
+Proof. by apply: (@nbhsB_subproof _ _ (GRing.Lmodule.class E)); exact: add_continuous. Qed.
 
 Lemma entourage_filter : Filter entourage.
 Proof.
@@ -216,13 +214,13 @@ Section Tvs_numDomain.
 Context (R : numDomainType) (E : tvsType R) (U : set E).
 
 Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U).
-Proof. exact/nbhs0N_subproof/scale_continuous. Qed.
+Proof. exact/(@nbhs0N_subproof _ _ (GRing.Lmodule.class E))/scale_continuous. Qed.
 
 Lemma nbhsT (x :E) : nbhs 0 U -> nbhs x (+%R x @` U).
-Proof. exact/nbhsT_subproof/add_continuous. Qed.
+Proof. exact/(@nbhsT_subproof _ _ (GRing.Lmodule.class E))/add_continuous. Qed.
 
 Lemma nbhsB (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U).
-Proof. exact/nbhsB_subproof/add_continuous. Qed.
+Proof. exact/(@nbhsB_subproof _ _ (GRing.Lmodule.class E))/add_continuous. Qed.
 
 End Tvs_numDomain.