Fix Tactics.descend_in_conjunctions on inductives with letins in constructors

dev/ci/user-overlays/21063-SkySkimmer-fix-apply-nreal.sh

@@ -0,0 +1 @@
+overlay vst https://github.com/SkySkimmer/VST fix-apply-nreal 21063

tactics/tactics.ml

@@ -1641,7 +1641,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
     | Some (_,_,isrec) ->
         (* At this point, ind is known to be an index-free one-constructor
            inductive type, potentially recursive. *)
-        let n = (constructors_nrealargs env ind).(0) in
+        let n = (constructors_nrealdecls env ind).(0) in
         let IndType (indf,_) = find_rectype env sigma ccl in
         let (_,inst), params = dest_ind_family indf in
         let cstr = (get_constructors env indf).(0) in

test-suite/bugs/bug_21036.v

@@ -0,0 +1,11 @@
+Definition  OK (b : bool) := if b then True else False.
+
+Inductive Foo (x y:bool) : Prop :=
+| is_Foo : let unused := True in OK x -> Foo x y.
+
+Lemma bug (h : OK true) : True.
+Proof.
+  apply is_Foo in h. (* would generate unbound rel *)
+  Validate Proof.
+  all:constructor.
+Qed.