diff options
Diffstat (limited to 'kernel/nativeinstr.mli')
| -rw-r--r-- | kernel/nativeinstr.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 9c17cc2b5..c319be32d 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -37,7 +37,7 @@ and lambda = (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) (* A fully applied constructor *) @@ -50,6 +50,10 @@ and lambda = | Llazy | Lforce +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = (constructor * Name.t array * lambda) array and fix_decl = Name.t array * lambda array * lambda array |