From 43880ca37594268573340b37acdf2d4b246a441b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 4 Sep 2025 17:02:53 +0200 Subject: [PATCH] Fix Tactics.descend_in_conjunctions on inductives with letins in constructors Fix #21036 Co-authored-by: yannl35133 --- .../user-overlays/21063-SkySkimmer-fix-apply-nreal.sh | 1 + tactics/tactics.ml | 2 +- test-suite/bugs/bug_21036.v | 11 +++++++++++ 3 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 dev/ci/user-overlays/21063-SkySkimmer-fix-apply-nreal.sh create mode 100644 test-suite/bugs/bug_21036.v 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.