Closes #13142 (more standardized pretty-printing of records).

2 files changed, 71 insertions, 0 deletions

diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index d45343fe60..7de1e7d559 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -30,3 +30,43 @@ fun '{| U := T; a := a; q := p |} => (T, p, a)
      : M -> Type * True * nat
 fun '{| U := T; a := a; q := p |} => (T, p, a)
      : M -> Type * True * nat
+{| a := 0; b := 0 |}
+     : T
+fun '{| |} => 0
+     : LongModuleName.test -> nat
+     = {|
+         a :=
+           {|
+             LongModuleName.long_field_name0 := 0;
+             LongModuleName.long_field_name1 := 1;
+             LongModuleName.long_field_name2 := 2;
+             LongModuleName.long_field_name3 := 3
+           |};
+         b :=
+           fun
+             '{|
+                LongModuleName.long_field_name0 := a;
+                LongModuleName.long_field_name1 := b;
+                LongModuleName.long_field_name2 := c;
+                LongModuleName.long_field_name3 := d
+              |} => (a, b, c, d)
+       |}
+     : T
+     = {|
+         a :=
+           {|
+             long_field_name0 := 0;
+             long_field_name1 := 1;
+             long_field_name2 := 2;
+             long_field_name3 := 3
+           |};
+         b :=
+           fun
+             '{|
+                long_field_name0 := a;
+                long_field_name1 := b;
+                long_field_name2 := c;
+                long_field_name3 := d
+              |} => (a, b, c, d)
+       |}
+     : T
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 71a8afa131..13ea37b11e 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -33,3 +33,34 @@ Check fun x:M => let 'D T _ p := x in T.
 Check fun x:M => let 'D T p := x in (T,p).
 Check fun x:M => let 'D T a p := x in (T,p,a).
 Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a).
+
+Module FormattingIssue13142.
+
+Record T {A B} := {a:A;b:B}.
+
+Module LongModuleName.
+  Record test := { long_field_name0 : nat;
+                  long_field_name1 : nat;
+                  long_field_name2 : nat;
+                  long_field_name3 : nat }.
+End LongModuleName.
+
+Definition c :=
+      {| LongModuleName.long_field_name0 := 0;
+         LongModuleName.long_field_name1 := 1;
+         LongModuleName.long_field_name2 := 2;
+         LongModuleName.long_field_name3 := 3 |}.
+
+Definition d :=
+ fun '{| LongModuleName.long_field_name0 := a;
+         LongModuleName.long_field_name1 := b;
+         LongModuleName.long_field_name2 := c;
+         LongModuleName.long_field_name3 := d |} => (a,b,c,d).
+
+Check {|a:=0;b:=0|}.
+Check fun '{| LongModuleName.long_field_name0:=_ |} => 0.
+Eval compute in {|a:=c;b:=d|}.
+Import LongModuleName.
+Eval compute in {|a:=c;b:=d|}.
+
+End FormattingIssue13142.