diff options
Diffstat (limited to 'theories/ZArith/ZOdiv_def.v')
| -rw-r--r-- | theories/ZArith/ZOdiv_def.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v index c73b6f091..88d573bb0 100644 --- a/theories/ZArith/ZOdiv_def.v +++ b/theories/ZArith/ZOdiv_def.v @@ -17,7 +17,7 @@ Definition NPgeb (a:N)(b:positive) := | Npos na => match Pcompare na b Eq with Lt => false | _ => true end end. -Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N := +Fixpoint Pdiv_eucl (a b:positive) : N * N := match a with | xH => match b with xH => (1, 0)%N | _ => (0, 1)%N end |