1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5321.v b/test-suite/bugs/closed/5321.v
new file mode 100644
index 00000000..03514e23
--- /dev/null
+++ b/test-suite/bugs/closed/5321.v
@@ -0,0 +1,18 @@
+Definition proj1_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
+  : proj1_sig u = proj1_sig v
+  := f_equal (@proj1_sig _ _) p.
+
+Definition proj2_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
+  : eq_rect _ _ (proj2_sig u) _ (proj1_sig_path p) = proj2_sig v
+  := match p with eq_refl => eq_refl end.
+
+Goal forall sz : nat,
+    let sz' := sz in
+    forall pf : sz = sz',
+      let feq_refl := exist (fun x : nat => sz = x) sz' eq_refl in
+      let fpf := exist (fun x : nat => sz = x) sz' pf in feq_refl = fpf -> 
+proj2_sig feq_refl = proj2_sig fpf.
+Proof.
+  intros.
+  etransitivity; [ | exact (proj2_sig_path H) ].
+  Fail clearbody fpf.