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).

---
 tactics/tactics.ml                 |  2 +-
 test-suite/bugs/closed/bug_12045.v | 19 +++++++++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_12045.v

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c79aca3d3c..8c4400a80f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4499,7 +4499,7 @@ let check_expected_type env sigma (elimc,bl) elimt =
   if n == 0 then error "Scheme cannot be applied.";
   let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
   let sigma = solve_evar_clause env sigma true cl bl in
-  let (_,u,_) = destProd sigma cl.cl_concl in
+  let (_,u,_) = destProd sigma (whd_all env sigma cl.cl_concl) in
   fun t -> match Evarconv.unify_leq_delay env sigma t u with
     | _sigma -> true
     | exception Evarconv.UnableToUnify _ -> false
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


From a44a478091416f17ecf47be4b254a742e9593441 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 17 Apr 2020 22:51:31 +0200
Subject: Change log for PR #12045.

---
 .../12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst  | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst

diff --git a/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst
new file mode 100644
index 0000000000..7af2b4d97b
--- /dev/null
+++ b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Anomaly with induction schemes whose conclusion is not normalized
+  (`#12116 <https://github.com/coq/coq/pull/12116>`_,
+  by Hugo Herbelin; fixes
+  `#12045 <https://github.com/coq/coq/pull/12045>`_)
-- 
cgit v1.2.3