From f71458c2d72d8cb2b534a1937ea1a259e9722edc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 17 Apr 2020 22:45:44 +0200
Subject: Fixing #12045 (missing normalization in conclusion of custom
 induction scheme).

---
 test-suite/bugs/closed/bug_12045.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12045.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3