diff options
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index cac2cc5b5..d3dfd2505 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v @@ -27,7 +27,7 @@ Ltac zarith := auto with zarith. Section POS_MOD. - Variable w:Set. + Variable w:Type. Variable w_0 : w. Variable w_digits : positive. Variable w_zdigits : w. @@ -201,7 +201,7 @@ End POS_MOD. Section DoubleDiv32. - Variable w : Set. + Variable w : Type. Variable w_0 : w. Variable w_Bm1 : w. Variable w_Bm2 : w. @@ -473,7 +473,7 @@ Section DoubleDiv32. End DoubleDiv32. Section DoubleDiv21. - Variable w : Set. + Variable w : Type. Variable w_0 : w. Variable w_0W : w -> zn2z w. @@ -634,7 +634,7 @@ Section DoubleDiv21. End DoubleDiv21. Section DoubleDivGt. - Variable w : Set. + Variable w : Type. Variable w_digits : positive. Variable w_0 : w. @@ -1344,7 +1344,7 @@ End DoubleDivGt. Section DoubleDiv. - Variable w : Set. + Variable w : Type. Variable w_digits : positive. Variable ww_1 : zn2z w. Variable ww_compare : zn2z w -> zn2z w -> comparison. |