diff options
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystem.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index ff2c23ab8..5c0d143c2 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -74,7 +74,7 @@ Section ModularBaseSystem. Definition carry_opp (carry_chain : list nat) (modulus_multiple : digits) (modulus_multiple_correct : decode modulus_multiple = 0%F) (x : digits) : digits := - carry_ carry_chain (opp modulus_multiple modulus_multiple_correct x). + carry_sub carry_chain modulus_multiple modulus_multiple_correct zero x. Definition rep (us : digits) (x : F modulus) := decode us = x. Local Notation "u ~= x" := (rep u x). |