diff options
| author | Pierre-Marie Pédrot | 2015-05-11 11:06:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-11 11:15:26 +0200 |
| commit | 138bd9756a0fc80647427b2894ba4485f3e6961b (patch) | |
| tree | 37a680bc27eae932604d777a843ab6efe9cd9ebd | |
| parent | 9a883e3740e21c93c8ea7f51b0cf0c4a76675773 (diff) | |
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.
| -rw-r--r-- | tactics/rewrite.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 |