diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Arith/Arith.v | 2 | ||||
| -rw-r--r-- | theories/Arith/Min.v | 2 | ||||
| -rw-r--r-- | theories/NArith/NArith.v | 4 | ||||
| -rw-r--r-- | theories/ZArith/ZArith.v | 2 |
4 files changed, 8 insertions, 2 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index b076de2aff..c522e01b3e 100644 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -18,3 +18,5 @@ Require Export Between. Require Export Peano_dec. Require Export Compare_dec. Require Export Factorial. + +Require Export ArithRing. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 3e64980cb7..d86d7f1169 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require Import Arith. +Require Import Le. Open Local Scope nat_scope. diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index a37387792b..5a2eeda484 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -11,4 +11,6 @@ (** Library for binary natural numbers *) Require Export BinPos. -Require Export BinNat.
\ No newline at end of file +Require Export BinNat. + +Require Export NArithRing. diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index 169a253fe6..5747afc9a2 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -19,3 +19,5 @@ Require Export Zsqrt. Require Export Zpower. Require Export Zdiv. Require Export Zlogarithm. + +Export ZArithRing. |