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 /kernel/nativecode.ml | |
| 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.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions