From 138bd9756a0fc80647427b2894ba4485f3e6961b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 May 2015 11:06:32 +0200
Subject: Fixing bug #4232.

We beta-iota normalize the type of the rewriting predicate to ensure that the
non-dependency in the arrow argument is meaningful. Otherwise, terms of the
form "forall x : A, (fun _ : A => P) x" generated by the retyping would confuse
the non-dependency heuristic.
---
 tactics/rewrite.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1be394aa4a..d487317736 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -226,6 +226,7 @@ end) = struct
       let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in
 	match kind_of_term t, l with
 	| Prod (na, ty, b), obj :: cstrs ->
+          let b = Reductionops.nf_betaiota (goalevars evars) b in
 	  if noccurn 1 b (* non-dependent product *) then
 	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
 	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
-- 
cgit v1.2.3