Merge PR #12572: Correctly classify variables as being unfoldable in dnet patterns.

Reviewed-by: SkySkimmer
Reviewed-by: maximedenes

1 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_12571.v b/test-suite/bugs/closed/bug_12571.v
new file mode 100644
index 0000000000..c348626921
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12571.v
@@ -0,0 +1,20 @@
+Axiom IsTrunc : Type -> Type.
+
+Existing Class IsTrunc.
+
+Declare Instance trunc_forall :
+  forall (A : Type) (P : A -> Type),
+  IsTrunc (forall a : A, P a).
+
+Axiom Graph : Set.
+Axiom in_N : forall (n : Graph), Type.
+
+Definition N : Type := @sigT Graph in_N.
+
+Goal forall (P : N -> Type)
+ (Q := fun m : Graph => forall mrec : in_N m, P (existT _ m mrec))
+ (A : Graph), IsTrunc (Q A).
+Proof.
+intros.
+solve [typeclasses eauto].
+Qed.