Improve previous fix

math-comp · May 7, 2023 · 497b612 · 497b612
1 parent fe0d4fd
commit 497b612
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/theories/signed.v b/theories/signed.v
@@ -317,9 +317,7 @@ Section POrder.
 Variables (d : unit) (T : porderType d) (x0 : T) (nz : nullity) (cond : reality).
 Local Notation sT := {compare x0 & nz & cond}.
 HB.instance Definition _ := [isSub for @Signed.r d T x0 nz cond].
-HB.instance Definition _ := [Choice of sT by <:].
-HB.instance Definition _ : Order.isPOrder d sT :=
-  Order.CancelPartial.Pcan d valK.
+HB.instance Definition _ : Order.POrder d sT := [POrder of sT by <:].
 End POrder.
 
 Lemma top_typ_subproof d (T : porderType d) (x0 x : T) :