diff options
Diffstat (limited to 'theories/Ints/num/NMake.v')
| -rw-r--r-- | theories/Ints/num/NMake.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v index 78fad0a0c7..6c8ae2f72f 100644 --- a/theories/Ints/num/NMake.v +++ b/theories/Ints/num/NMake.v @@ -799,7 +799,7 @@ Module Make (W0:W0Type). let op := make_op n in match op.(znz_sub_c) x y with | C0 r => Nn n r - | C1 r => Nn (S n) (WW op.(znz_1) r) end. + | C1 r => N0 w_0 end. Definition sub x y := match x, y with |