fixes #901 (#907)

* fixes #901

CHANGELOG_UNRELEASED.md

@@ -14,6 +14,12 @@
 
 ### Removed
 
+- in `normedtype.v`:
+  + instance `Proper_dnbhs_realType`
+- in `measure.v`:
+  + instances `ae_filter_algebraOfSetsType`, `ae_filter_measurableType`,
+  `ae_properfilter_measurableType`
+
 ### Infrastructure
 
 ### Misc

theories/derive.v

@@ -1360,8 +1360,6 @@ Lemma cvg_at_rightE (R : numFieldType) (V : normedModType R) (f : R -> V) x :
   cvg (f @ x^') -> lim (f @ x^') = lim (f @ at_right x).
 Proof.
 move=> cvfx; apply/Logic.eq_sym.
-(* should be inferred *)
-have atrF := at_right_proper_filter x.
 apply: (@cvg_lim _ _ _ (at_right _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
 by exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
 Qed.
@@ -1371,8 +1369,6 @@ Lemma cvg_at_leftE (R : numFieldType) (V : normedModType R) (f : R -> V) x :
   cvg (f @ x^') -> lim (f @ x^') = lim (f @ at_left x).
 Proof.
 move=> cvfx; apply/Logic.eq_sym.
-(* should be inferred *)
-have atrF := at_left_proper_filter x.
 apply: (@cvg_lim _ _ _ (at_left _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
 exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _].
 by apply: xe_A => //; rewrite eq_sym.

theories/measure.v

@@ -3076,12 +3076,6 @@ by split; [exact: almost_everywhereT|exact: almost_everywhereI|
   exact: almost_everywhereS].
 Qed.
 
-#[global]
-Instance ae_filter_algebraOfSetsType d {T : algebraOfSetsType d}
-    (R : realFieldType) (mu : {measure set T -> \bar R}) :
-  Filter (almost_everywhere mu).
-Proof. exact: ae_filter_ringOfSetsType. Qed.
-
 #[global]
 Instance ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d}
     (R : realFieldType) (mu : {measure set T -> \bar R}) :
@@ -3092,19 +3086,13 @@ rewrite /almost_everywhere setC0 => /(measure_negligible measurableT).
 by apply/eqP; rewrite eq_le negb_and measure_ge0 orbF -ltNge.
 Qed.
 
-#[global]
-Instance ae_filter_measurableType d {T : measurableType d}
-    (R : realFieldType) (mu : {measure set T -> \bar R}) :
-  Filter (almost_everywhere mu).
-Proof. exact: ae_filter_ringOfSetsType. Qed.
+End ae.
 
-#[global]
-Instance ae_properfilter_measurableType d {T : measurableType d}
-    (R : realFieldType) (mu : {measure set T -> \bar R}) :
-  mu [set: T] > 0 -> ProperFilter (almost_everywhere mu).
-Proof. exact: ae_properfilter_algebraOfSetsType. Qed.
+#[global] Hint Extern 0 (Filter (almost_everywhere _)) =>
+  (apply: ae_filter_ringOfSetsType) : typeclass_instances.
 
-End ae.
+#[global] Hint Extern 0 (ProperFilter (almost_everywhere _)) =>
+  (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances.
 
 Definition almost_everywhere_notation d (T : semiRingOfSetsType d)
     (R : realFieldType) (mu : set T -> \bar R) (P : T -> Prop)

theories/normedtype.v

@@ -367,9 +367,8 @@ rewrite /ball /= opprD addrA subrr distrC subr0 ger0_norm //.
 by rewrite {2}(splitr e%:num) ltr_spaddl.
 Qed.
 
-Global Instance Proper_dnbhs_realType (R : realType) (x : R) :
-  ProperFilter x^'.
-Proof. exact: Proper_dnbhs_numFieldType. Qed.
+#[global] Hint Extern 0 (ProperFilter _^') =>
+  (apply: Proper_dnbhs_numFieldType) : typeclass_instances.
 
 (** * Some Topology on extended real numbers *)
 
@@ -2124,6 +2123,11 @@ Arguments cvgr_neq0 {R V T F FF f}.
   H : x \is_near _ |- _ => near: x; exact: nbhs_left_le end : core.
 
 
+#[global] Hint Extern 0 (ProperFilter _^'-) =>
+  (apply: at_left_proper_filter) : typeclass_instances.
+#[global] Hint Extern 0 (ProperFilter _^'+) =>
+  (apply: at_right_proper_filter) : typeclass_instances.
+
 Section at_left_rightR.
 Variable (R : numFieldType).