aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativeinstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativeinstr.mli')
-rw-r--r--kernel/nativeinstr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index cb79877e8..2353470f0 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -30,7 +30,7 @@ and lambda =
| Lapp of lambda * lambda array
| Lconst of prefix * pconstant
| Lproj of prefix * constant (* prefix, projection name *)
- | Lprim of prefix * constant * Primitives.t * lambda array
+ | Lprim of prefix * constant * CPrimitives.t * lambda array
| Lcase of annot_sw * lambda * lambda * lam_branches
(* annotations, term being matched, accu, branches *)
| Lif of lambda * lambda * lambda