fix

Author: affeldt-aist

classical/classical_sets.v

@@ -2463,17 +2463,6 @@ HB.instance Definition _ m n (T : pointedType) :=
 HB.instance Definition _ (T : choiceType) := isPointed.Build (option T) None.
 HB.instance Definition _ (T : choiceType) := isPointed.Build {fset T} fset0.
 
-HB.instance Definition _ {R : numDomainType} (E F : lmodType R) :=
-  isPointed.Build {linear E -> F} (Algebra.null_fun _).
-
-(*Section coucou.
-Context {R : numDomainType} (E F : lmodType R).
-
-Check (point : {linear E -> F}%R).*)
-
-
-
-
 Notation get := (xget point).
 Notation "[ 'get' x | E ]" := (get [set x | E])
   (at level 0, x name, format "[ 'get'  x  |  E ]", only printing) : form_scope.

classical/functions.v

@@ -2782,7 +2782,7 @@ Section Sub.
 Context (f : E -> F) (fP : f \in linfun).
 
 Definition linfun_Sub_subproof :=
-  @GRing.isLinear.Build _ E F s f  (set_mem fP).
+  @GRing.isLinear.Build _ E F s f (set_mem fP).
 
 #[local] HB.instance Definition _ := linfun_Sub_subproof.
 Definition linfun_Sub : {linear _  -> _ | _ } := f.