diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Int31/Cyclic31.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 7d795cf50e..744f2f47cc 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1140,7 +1140,7 @@ Definition int31_op := (mk_znz_op w_iszero (* Basic arithmetic operations *) (fun i => 0 -c i) - (fun i => 0 - i) + opp31 (fun i => 0-i-1) (fun i => i +c 1) add31c |