5 files changed, 180 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/bug_13171.v b/test-suite/bugs/closed/bug_13171.v
new file mode 100644
index 0000000000..0564722729
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13171.v
@@ -0,0 +1,10 @@
+Primitive array := #array_type.
+
+Goal False.
+Proof.
+  unshelve epose (_:nat). exact_no_check true.
+  Fail let c := open_constr:([| n | 0 |]) in
+       let c := eval cbv in c in
+       let c := type of c in
+       idtac c.
+Abort.
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.
diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
index 773533a8d3..17c1aaa55b 100644
--- a/test-suite/output/goal_output.out
+++ b/test-suite/output/goal_output.out
@@ -2,7 +2,79 @@ Nat.t = nat
      : Set
 Nat.t = nat
      : Set
+2 subgoals
+  
+  ============================
+  True
+
+subgoal 2 is:
+ True
+2 subgoals, subgoal 1 (?Goal)
+  
+  ============================
+  True
+
+subgoal 2 (?Goal0) is:
+ True
 1 subgoal
   
   ============================
-  False
+  True
+1 subgoal (?Goal0)
+  
+  ============================
+  True
+1 subgoal (?Goal0)
+  
+  ============================
+  True
+
+*** Unfocused goals:
+
+subgoal 2 (?Goal1) is:
+ True
+subgoal 3 (?Goal) is:
+ True
+1 subgoal
+  
+  ============================
+  True
+
+*** Unfocused goals:
+
+subgoal 2 is:
+ True
+subgoal 3 is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+2 subgoals
+
+subgoal 1 is:
+ True
+subgoal 2 is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+2 subgoals
+
+subgoal 1 (?Goal0) is:
+ True
+subgoal 2 (?Goal) is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+1 subgoal
+
+subgoal 1 is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+1 subgoal
+
+subgoal 1 (?Goal) is:
+ True
diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v
index 327b80b0aa..b1ced94054 100644
--- a/test-suite/output/goal_output.v
+++ b/test-suite/output/goal_output.v
@@ -6,8 +6,32 @@
 Print Nat.t.
 Timeout 1 Print Nat.t.
 
-Lemma toto: False.
 Set Printing All.
+Lemma toto: True/\True.
+Proof.
+split.
 Show.
+Set Printing Goal Names.
+Show.
+Unset Printing Goal Names.
+assert True.
+- idtac.
+Show.
+Set Printing Goal Names.
+Show.
+Set Printing Unfocused.
+Show.
+Unset Printing Goal Names.
+Show.
+Unset Printing Unfocused.
+  auto.
+Show.
+Set Printing Goal Names.
+Show.
+Unset Printing Goal Names.
+- auto.
+Show.
+Set Printing Goal Names.
+Show.
+Unset Printing Goal Names.
 Abort.
-