Revert "Re-export numeric subclass instances"

This reverts commit 91fd951.

Author: MatthewDaggitt

src/Data/Integer/Base.agda

@@ -14,7 +14,7 @@ module Data.Integer.Base where
 open import Algebra.Bundles.Raw
   using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing)
 open import Data.Bool.Base using (Bool; T; true; false)
-open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s) hiding (module ℕ)
+open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s)
 open import Data.Sign.Base as Sign using (Sign)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
@@ -140,9 +140,6 @@ record Negative (i : ℤ) : Set where
 
 -- Instances
 
-open ℕ public
-  using (nonZero)
-
 instance
   pos : ∀ {n} → Positive +[1+ n ]
   pos = _

src/Data/Rational/Base.agda

@@ -10,9 +10,7 @@ module Data.Rational.Base where
 
 open import Algebra.Bundles.Raw
 open import Data.Bool.Base using (Bool; true; false; if_then_else_)
-open import Data.Integer.Base as ℤ
-  using (ℤ; +_; +0; +[1+_]; -[1+_])
-  hiding (module ℤ)
+open import Data.Integer.Base as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_])
 open import Data.Nat.GCD
 open import Data.Nat.Coprimality as C
   using (Coprime; Bézout-coprime; coprime-/gcd; coprime?; ¬0-coprimeTo-2+)
@@ -178,11 +176,6 @@ NonPositive p = ℚᵘ.NonPositive (toℚᵘ p)
 NonNegative : Pred ℚ 0ℓ
 NonNegative p = ℚᵘ.NonNegative (toℚᵘ p)
 
--- Instances
-
-open ℤ public
-  using (nonZero; pos; nonNeg; nonPos0; nonPos; neg)
-
 -- Constructors
 
 ≢-nonZero : ∀ {p} → p ≢ 0ℚ → NonZero p
@@ -209,12 +202,6 @@ nonPositive {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonPositive {toℚᵘ p} (
 nonNegative : ∀ {p} → p ≥ 0ℚ → NonNegative p
 nonNegative {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonNegative {toℚᵘ p} (ℚᵘ.*≤* p≤q)
 
--- Re-export base instances so that users don't have to open
--- Data.Nat.Base.
-
-open ℕ public
-  using (nonZero)
-
 ------------------------------------------------------------------------
 -- Operations on rationals
 

src/Data/Rational/Unnormalised/Base.agda

@@ -12,7 +12,6 @@ open import Algebra.Bundles.Raw
 open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Data.Integer.Base as ℤ
   using (ℤ; +_; +0; +[1+_]; -[1+_]; +<+; +≤+)
-  hiding (module ℤ)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Level using (0ℓ)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
@@ -150,11 +149,6 @@ NonPositive p = ℤ.NonPositive (↥ p)
 NonNegative : Pred ℚᵘ 0ℓ
 NonNegative p = ℤ.NonNegative (↥ p)
 
--- Instances
-
-open ℤ public
-  using (nonZero; pos; nonNeg; nonPos0; nonPos; neg)
-
 -- Constructors and destructors
 
 -- Note: these could be proved more elegantly using the constructors