Replace record directive "eta-equality" by "no-eta-equality;pattern"

Future Agda might not allow unguarded record types with eta-equality
in the safe mode anymore.

So we switch eta off here, but make the constructor a pattern so that
it can still be matched on.

Re: agda/agda#7470

Author: andreasabel

src/Data/Record.agda

@@ -63,8 +63,9 @@ mutual
   -- inferred from a value of type Record Sig.
 
   record Record {s} (Sig : Signature s) : Set s where
-    eta-equality
     inductive
+    no-eta-equality
+    pattern
     constructor rec
     field fun : Record-fun Sig
 

src/Tactic/RingSolver/Core/Polynomial/Base.agda

@@ -130,8 +130,9 @@ Normalised : ∀ {i} → Coeff i + → Set
 infixl 6 _⊐_
 record Poly n where
   inductive
+  no-eta-equality
+  pattern  -- To allow matching on constructor
   constructor _⊐_
-  eta-equality  -- To allow matching on constructor
   field
     {i}  : ℕ
     flat : FlatPoly i