diff options
| -rw-r--r-- | contrib/ring/ArithRing.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v index e89017daf7..0a49ecb476 100644 --- a/contrib/ring/ArithRing.v +++ b/contrib/ring/ArithRing.v @@ -14,6 +14,9 @@ Require Export Ring. Require Export Arith. Require Eqdep_dec. +V7only [Import nat_scope.]. +Open Local Scope nat_scope. + Fixpoint nateq [n,m:nat] : bool := Cases n m of | O O => true |