diff options
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystem.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 4fd881e1e..f80ce05f8 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -37,9 +37,9 @@ Section ModularBaseSystem. from_list (sub [[modulus_multiple]] [[us]] [[vs]]) (length_sub length_to_list length_to_list length_to_list). - Definition zero : digits := encode (ZToField 0). + Definition zero : digits := encode (ZToField _ 0). - Definition one : digits := encode (ZToField 1). + Definition one : digits := encode (ZToField _ 1). (* Placeholder *) Definition opp (x : digits) : digits := encode (ModularArithmetic.opp (decode x)). |