Merge PR #12572: Correctly classify variables as being unfoldable in …

…dnet patterns.

Reviewed-by: SkySkimmer
Reviewed-by: maximedenes

doc/changelog/04-tactics/12572-fix-12571.rst

@@ -0,0 +1,6 @@
+- **Fixed:**
+  typeclasses eauto (and discriminated hint bases) now correctly
+  classify local variables as being unfoldable
+  (`#12572 <https://github.com/coq/coq/pull/12572>`_,
+  fixes `#12571 <https://github.com/coq/coq/issues/12571>`_,
+  by Pierre-Marie Pédrot).

tactics/btermdn.ml

@@ -77,15 +77,16 @@ let constr_val_discr_st sigma ts t =
     | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l)
     | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
     | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
-    | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l)
+    | Var id -> if TransparentState.is_transparent_variable ts id then Everything else Label(GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Label(ProdLabel, [d; c])
     | Lambda (n, d, c) ->
       if List.is_empty l then
         Label(LambdaLabel, [d; c] @ l)
       else Everything
     | Sort _ -> Label(SortLabel, [])
     | Evar _ -> Everything
-    | _ -> Nothing
+    | Rel _ | Meta _ | Cast _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _
+    | Proj _ | Int _ | Float _ -> Nothing
 
 let constr_pat_discr_st ts t =
   let open GlobRef in

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.