diff options
| author | Matthieu Sozeau | 2018-09-07 13:23:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-09-07 14:06:17 +0200 |
| commit | e3e9300a2444f5d2e595a63bf63c91e61653d77d (patch) | |
| tree | ec2e0ea492d5c4abf085385cb0b1f2797c1ff0ee /kernel/vmvalues.ml | |
| parent | 07c3905c30590c93f1b173833087bbd1df364227 (diff) | |
Fix bug #8432 : program fixpoint and universes
One didn't normalize the bodies of fixpoints according to the universe
context, resulting in a type errors. Use EConstr.to_constr to ensure
universes are normalized instead of using EConstr.Unsafe.to_constr.
Diffstat (limited to 'kernel/vmvalues.ml')
0 files changed, 0 insertions, 0 deletions