porting quotient fixes

math-comp · Mar 29, 2023 · 7ce6f23 · 7ce6f23
1 parent c665e8b
commit 7ce6f23
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/theories/topology.v b/theories/topology.v
@@ -4871,9 +4871,10 @@ Context {T : topologicalType} {Q0 : quotType T}.
 
 Local Notation Q := (quotient_topology Q0).
 
-HB.instance Definition _ := gen_eqMixin Q.
-HB.instance Definition _ := gen_choiceMixin Q.
-HB.instance Definition _ := isPointed.Build Q (\pi_Q point).
+HB.instance Definition _ := Quotient.copy Q Q0.
+HB.instance Definition _ := [Sub Q of T by %/].
+HB.instance Definition _ := [Choice of Q by <:].
+HB.instance Definition _ := isPointed.Build Q (\pi_Q point : Q).
 
 Definition quotient_open U := open (\pi_Q @^-1` U).