diff options
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index fe77bf5c7..54134f95b 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v @@ -149,9 +149,9 @@ Section DoubleBase. Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[[ x ]]" := (ww_to_Z x) (at level 0, x at level 99). Notation "[+[ c ]]" := - (interp_carry 1 wwB ww_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wwB ww_to_Z c) (at level 0, c at level 99). Notation "[-[ c ]]" := - (interp_carry (-1) wwB ww_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wwB ww_to_Z c) (at level 0, c at level 99). Notation "[! n | x !]" := (double_to_Z n x) (at level 0, x at level 99). Variable spec_w_0 : [|w_0|] = 0. |