Stop Data.Rational.Base exporting +0 and +[1+_] (#1537)

Author: MatthewDaggitt

CHANGELOG.md

@@ -53,6 +53,10 @@ Non-backwards compatible changes
   So `[a-zA-Z]+.agdai?` run on "the path _build/Main.agdai corresponds to"
   will return "Main.agdai" when it used to be happy to just return "n.agda".
 
+* The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer 
+  exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)`
+  directly to use them.
+
 Deprecated modules
 ------------------
 

src/Data/Rational/Base.agda

@@ -10,7 +10,7 @@ module Data.Rational.Base where
 
 open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Function.Base using (id)
-open import Data.Integer.Base as ℤ using (ℤ; +_; +0; -[1+_])
+open import Data.Integer.Base as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_])
 import Data.Integer.GCD as ℤ
 import Data.Integer.DivMod as ℤ
 open import Data.Nat.GCD
@@ -35,13 +35,6 @@ open import Relation.Binary.PropositionalEquality
 
 open ≡-Reasoning
 
--- Note, these are re-exported publicly to maintain backwards
--- compatability. Although we are unable (?) to put a warning on them,
--- using these from `Data.Rational` should be viewed as a deprecated
--- feature.
-
-open import Data.Integer public using (+0; +[1+_])
-
 ------------------------------------------------------------------------
 -- Rational numbers in reduced form. Note that there is exactly one
 -- way to represent every rational number.

src/Data/Rational/Properties.agda

@@ -20,7 +20,7 @@ import Algebra.Morphism.RingMonomorphism as RingMonomorphisms
 import Algebra.Morphism.LatticeMonomorphism as LatticeMonomorphisms
 import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
 open import Data.Bool.Base using (T; true; false)
-open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; 0ℤ; 1ℤ; _◃_)
+open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; +[1+_]; +0; 0ℤ; 1ℤ; _◃_)
 open import Data.Integer.Coprimality using (coprime-divisor)
 import Data.Integer.Properties as ℤ
 open import Data.Integer.GCD using (gcd; gcd[i,j]≡0⇒i≡0; gcd[i,j]≡0⇒j≡0)