diff options
Diffstat (limited to 'kernel/nativeinstr.mli')
| -rw-r--r-- | kernel/nativeinstr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index bba011475..13d61841f 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -29,6 +29,7 @@ and lambda = | Llet of name * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * constant + | Lprim of prefix * constant * Primitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda |