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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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