diff options
| author | Pierre-Marie Pédrot | 2020-10-26 12:42:00 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-26 12:51:12 +0100 |
| commit | 560187914e88790cef9787904874df8517aa157c (patch) | |
| tree | 73ec1001ef3b5867a59e85aa9566f044d2f8aa80 /kernel/nativecode.ml | |
| parent | 9e7b0f9f248a1fae8e5681815bd621f182696c4f (diff) | |
Fix bug in conversion of primitive values.
A partially applied primitive was considered CClosure.Norm, i.e. neutral. But
this is not true, because substituting this term as the head of an application
may trigger further reduction. In this respect, primitive functions behave like
fixpoints.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions