Merge PR #12116: Fixing #12045: missing normalization in conclusion of custom induction scheme

Reviewed-by: ppedrot

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_12045.v b/test-suite/bugs/closed/bug_12045.v
new file mode 100644
index 0000000000..4e416778a9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12045.v
@@ -0,0 +1,19 @@
+(* Check enough reduction happens in the conclusion of an induction scheme *)
+
+Lemma foo :
+  forall (P : nat -> Prop),
+    (forall n, P (S n)) ->
+    forall n,
+      (fun e =>
+         IsSucc e ->
+         P e) n.
+Proof.
+Admitted.
+
+Theorem bar : forall n,
+    IsSucc n ->
+    True.
+Proof.
+  intros.
+  Fail induction n using foo. (* was an anomaly *)
+Admitted.