diff --git a/dev/ci/user-overlays/21063-SkySkimmer-fix-apply-nreal.sh b/dev/ci/user-overlays/21063-SkySkimmer-fix-apply-nreal.sh
new file mode 100644
index 000000000000..e4328999be03
--- /dev/null
+++ b/dev/ci/user-overlays/21063-SkySkimmer-fix-apply-nreal.sh
@@ -0,0 +1 @@
+overlay vst https://github.com/SkySkimmer/VST fix-apply-nreal 21063
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c3c992add2a1..c2603b70c455 100644
--- a/tactics/tactics.ml
+++ b/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
diff --git a/test-suite/bugs/bug_21036.v b/test-suite/bugs/bug_21036.v
new file mode 100644
index 000000000000..38d45bb34fa1
--- /dev/null
+++ b/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.