Skip to content

Commit 52e4bdb

Browse files
affeldt-aistaffeldt-aist
committed
rm unproductive HB.instance
1 parent 2434d56 commit 52e4bdb

12 files changed

Lines changed: 50 additions & 30 deletions

File tree

‎classical/functions.v‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -647,7 +647,8 @@ HB.instance Definition _ (f : {oinvfun A >-> B}) := Fun.on (oapp f).
647647
HB.instance Definition _ (f : {injfun A >-> B}) := Fun.on (oapp f).
648648
HB.instance Definition _ (f : {surjfun A >-> B}) := Fun.on (oapp f).
649649
HB.instance Definition _ (f : {bij A >-> B}) := Fun.on (oapp f).
650-
HB.instance Definition _ (f : {splitbij A >-> B}) := Fun.on (oapp f).
650+
(*HB.instance Definition _ (f : {splitbij A >-> B}) := Fun.on (oapp f).*)
651+
(* generates: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
651652

652653
End OApply.
653654

‎reals/prodnormedzmodule.v‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,13 +21,16 @@ Import Order.TTheory GRing.Theory Num.Theory.
2121

2222
Section Linear1.
2323
Context (R : pzRingType) (U : lmodType R) (V : zmodType) (s : R -> V -> V).
24-
HB.instance Definition _ := gen_eqMixin {linear U -> V | s}.
25-
HB.instance Definition _ := gen_choiceMixin {linear U -> V | s}.
24+
(*HB.instance Definition _ := gen_eqMixin {linear U -> V | s}.*)
25+
(*Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]*)
26+
(*HB.instance Definition _ := gen_choiceMixin {linear U -> V | s}.*)
27+
(*Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]*)
2628
End Linear1.
2729
Section Linear2.
2830
Context (R : pzRingType) (U : lmodType R) (V : zmodType) (s : GRing.Scale.law R V).
29-
HB.instance Definition _ :=
30-
isPointed.Build {linear U -> V | GRing.Scale.Law.sort s} \0.
31+
(*HB.instance Definition _ :=
32+
isPointed.Build {linear U -> V | GRing.Scale.Law.sort s} \0.*)
33+
(*Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]*)
3134
End Linear2.
3235

3336
Module ProdNormedZmodule.

‎theories/hoelder.v‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -939,7 +939,8 @@ HB.instance Definition _ :=
939939
Lemma LfuneqP (f g : LfunType mu p1) : f = g <-> f =1 g.
940940
Proof. by split=> [->//|fg]; exact/val_inj/funext. Qed.
941941

942-
HB.instance Definition _ := [Choice of LfunType mu p1 by <:].
942+
(*HB.instance Definition _ := [Choice of LfunType mu p1 by <:].*)
943+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
943944

944945
Lemma finite_norm_cst0 : finite_norm mu p (cst 0).
945946
Proof. by rewrite /finite_norm Lnorm0// gt_eqF// (lt_le_trans _ p1). Qed.

‎theories/lebesgue_integral_theory/lebesgue_integral_fubini.v‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -373,8 +373,9 @@ split; first exact: measurableX.
373373
by rewrite product_measure1E// lte_mul_pinfty// ge0_fin_numE.
374374
Qed.
375375

376-
HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)
377-
product_measure_sigma_finite.
376+
(*HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)
377+
product_measure_sigma_finite.*)
378+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
378379

379380
Lemma product_measure_unique
380381
(m' : {measure set (T1 * T2) -> \bar R}) :

‎theories/lebesgue_integral_theory/measurable_fun_approximation.v‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -381,12 +381,14 @@ Variables (D : set T) (mD : measurable D) (mf : measurable_fun D f).
381381

382382
Import HBSimple.
383383
(* NB: already instantiated in cardinality.v *)
384-
HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x).
384+
(*HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x).*)
385+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
385386

386387
Import HBNNSimple.
387388
(* NB: already instantiated in lebesgue_integral.v *)
388-
HB.instance Definition _ x : @NonNegFun T R (cst x%:num) :=
389-
NonNegFun.on (cst x%:num).
389+
(*HB.instance Definition _ x : @NonNegFun T R (cst x%:num) :=
390+
NonNegFun.on (cst x%:num).*)
391+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
390392

391393
Lemma approximation_sfun :
392394
exists g : {sfun T >-> R}^nat, (forall x, D x -> EFin \o g ^~ x @ \oo --> f x).

‎theories/measure_theory/measurable_structure.v‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1584,7 +1584,8 @@ Let prod_salgebra_bigcup (F : _^nat) :
15841584
g_sigma_preimageU f1 f2 (\bigcup_i (F i)).
15851585
Proof. exact: sigma_algebra_bigcup. Qed.
15861586

1587-
HB.instance Definition _ := Choice.on (T1 * T2)%type.
1587+
(*HB.instance Definition _ := Choice.on (T1 * T2)%type.*)
1588+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
15881589
HB.instance Definition prod_salgebra_mixin :=
15891590
@isMeasurable.Build (measure_prod_display (d1, d2))
15901591
(T1 * T2)%type (g_sigma_preimageU f1 f2)

‎theories/normedtype_theory/normed_module.v‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -221,8 +221,9 @@ HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
221221
HB.instance Definition _ := Vector.copy R R^o.
222222
#[export, non_forgetful_inheritance]
223223
HB.instance Definition _ := NormedModule.copy R R^o.
224-
#[export, non_forgetful_inheritance]
225-
HB.instance Definition _ := Num.RealField.on R.
224+
(*#[export, non_forgetful_inheritance]
225+
HB.instance Definition _ := Num.RealField.on R.*)
226+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
226227
End realFieldType.
227228

228229
Section numClosedFieldType.
@@ -245,8 +246,9 @@ HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
245246
HB.instance Definition _ := Vector.copy R R^o.
246247
#[export, non_forgetful_inheritance]
247248
HB.instance Definition _ := NormedModule.copy R R^o.
248-
#[export, non_forgetful_inheritance]
249-
HB.instance Definition _ := Num.NumField.on R.
249+
(*#[export, non_forgetful_inheritance]
250+
HB.instance Definition _ := Num.NumField.on R.*)
251+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
250252
End numFieldType.
251253

252254
Module Exports. Export numFieldTopology.Exports. HB.reexport. End Exports.

‎theories/normedtype_theory/urysohn.v‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -746,7 +746,8 @@ Definition type : Type := let _ := completely_regular_nbhsE in X.
746746
(@entourage_inv X')
747747
(@entourage_split_ex X')
748748
completely_regular_nbhsE.
749-
#[export] HB.instance Definition _ := Uniform.on type.
749+
(*#[export] HB.instance Definition _ := Uniform.on type.*)
750+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
750751

751752
End completely_regular_uniformity.
752753
Module Exports. HB.reexport. End Exports.

‎theories/topology_theory/function_spaces.v‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -567,10 +567,11 @@ HB.instance Definition _ (U : topologicalType) (T : uniformType) :=
567567
(continuousType U T)
568568
(initial_topology (id : continuousType U T -> (U -> T))).
569569

570-
HB.instance Definition _ (U : topologicalType) (R : realType)
570+
(*HB.instance Definition _ (U : topologicalType) (R : realType)
571571
(T : pseudoMetricType R) :=
572572
PseudoMetric.on
573-
(initial_topology (id : continuousType U T -> (U -> T))).
573+
(initial_topology (id : continuousType U T -> (U -> T))).*)
574+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
574575

575576
End ArrowAsUniformType.
576577

‎theories/topology_theory/matrix_topology.v‎

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -145,16 +145,21 @@ by apply: filter_bigI => ??; apply: entP.
145145
Unshelve. all: by end_near. Qed.
146146

147147
Section matrix_PointedTopology.
148-
Variables (m n : nat) .
148+
Variables (m n : nat).
149149
HB.instance Definition _ (T : ptopologicalType) := Filtered.on 'M[T]_(m, n).
150-
HB.instance Definition _ (T : ptopologicalType) := Pointed.on 'M[T]_(m, n).
151-
HB.instance Definition _ (T : ptopologicalType) :=
152-
PointedFiltered.on 'M[T]_(m, n).
153-
HB.instance Definition _ (T : ptopologicalType) :=
154-
PointedTopological.on 'M[T]_(m, n).
155-
HB.instance Definition _ (T : uniformType) := Uniform.on 'M[T]_(m, n).
150+
(*HB.instance Definition _ (T : ptopologicalType) := Pointed.on 'M[T]_(m, n).*)
151+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
152+
(*HB.instance Definition _ (T : ptopologicalType) :=
153+
PointedFiltered.on 'M[T]_(m, n).*)
154+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
155+
(*HB.instance Definition _ (T : ptopologicalType) :=
156+
PointedTopological.on 'M[T]_(m, n).*)
157+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
158+
(*HB.instance Definition _ (T : uniformType) := Uniform.on 'M[T]_(m, n).*)
159+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
156160
HB.instance Definition _ (T : puniformType) := Pointed.on 'M[T]_(m, n).
157-
HB.instance Definition _ (T : puniformType) := PointedUniform.on 'M[T]_(m, n).
161+
(*HB.instance Definition _ (T : puniformType) := PointedUniform.on 'M[T]_(m, n).*)
162+
(* generates Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] *)
158163
End matrix_PointedTopology.
159164

160165
Section matrix_Complete.

0 commit comments

Comments
 (0)