Make sure RawRing defines rawRingWithoutOne (#1967)

Author: Taneb

src/Algebra/Bundles/Raw.agda

@@ -213,14 +213,18 @@ record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
     ; *-rawMagma; *-rawMonoid
     )
 
-  +-rawGroup : RawGroup c ℓ
-  +-rawGroup = record
+  rawRingWithoutOne : RawRingWithoutOne c ℓ
+  rawRingWithoutOne = record
     { _≈_ = _≈_
-    ; _∙_ = _+_
-    ; ε   = 0#
-    ; _⁻¹ = -_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; -_ = -_
+    ; 0# = 0#
     }
 
+  open RawRingWithoutOne rawRingWithoutOne public
+    using (+-rawGroup)
+
 ------------------------------------------------------------------------
 -- Raw bundles with 3 binary operations
 ------------------------------------------------------------------------