[ re #5770 ] Add --erase-record-parameters to three Builtin modules that use {{...}} syntaxrefs/pull/5771/headerase-record-parameters

4 files changed, 7 insertions, 7 deletions

diff --git a/src/data/lib/prim/Agda/Builtin/FromNat.agda b/src/data/lib/prim/Agda/Builtin/FromNat.agda
index 1f61e3e..a008870 100644
--- a/src/data/lib/prim/Agda/Builtin/FromNat.agda
+++ b/src/data/lib/prim/Agda/Builtin/FromNat.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}
+{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness --erase-record-parameters #-}
 
 module Agda.Builtin.FromNat where
 
diff --git a/src/data/lib/prim/Agda/Builtin/FromNeg.agda b/src/data/lib/prim/Agda/Builtin/FromNeg.agda
index 046a4ed..40509bf 100644
--- a/src/data/lib/prim/Agda/Builtin/FromNeg.agda
+++ b/src/data/lib/prim/Agda/Builtin/FromNeg.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}
+{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness --erase-record-parameters #-}
 
 module Agda.Builtin.FromNeg where
 
diff --git a/src/data/lib/prim/Agda/Builtin/FromString.agda b/src/data/lib/prim/Agda/Builtin/FromString.agda
index ab1ed65..bada64e 100644
--- a/src/data/lib/prim/Agda/Builtin/FromString.agda
+++ b/src/data/lib/prim/Agda/Builtin/FromString.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}
+{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness --erase-record-parameters #-}
 
 module Agda.Builtin.FromString where
 
diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
index 5480dc6..e4c67ca 100644
--- a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
+++ b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
@@ -270,12 +270,12 @@ instance EmbPrj Doc where
 
 instance EmbPrj PragmaOptions where
   icod_ = \case
-    PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ddd ->
-      icodeN' PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ddd
+    PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ddd eee ->
+      icodeN' PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ddd eee
 
   value = vcase $ \case
-    [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, aa, bb, cc, dd, ee, ff, gg, hh, ii, jj, kk, ll, mm, nn, oo, pp, qq, rr, ss, tt, uu, vv, ww, xx, yy, zz, aaa, bbb, ccc, ddd] ->
-      valuN PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ddd
+    [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, aa, bb, cc, dd, ee, ff, gg, hh, ii, jj, kk, ll, mm, nn, oo, pp, qq, rr, ss, tt, uu, vv, ww, xx, yy, zz, aaa, bbb, ccc, ddd, eee] ->
+      valuN PragmaOptions a b c d e f g h i j k l m n o p q r s t u v w x y z aa bb cc dd ee ff gg hh ii jj kk ll mm nn oo pp qq rr ss tt uu vv ww xx yy zz aaa bbb ccc ddd eee
     _ -> malformed
 
 instance EmbPrj ProfileOptions where