aboutsummaryrefslogtreecommitdiff
path: root/kernel/cinstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cinstr.mli')
-rw-r--r--kernel/cinstr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
index 3afef339fb..171ca38830 100644
--- a/kernel/cinstr.mli
+++ b/kernel/cinstr.mli
@@ -36,7 +36,7 @@ and lambda =
| Lval of structured_constant
| Lsort of Sorts.t
| Lind of pinductive
- | Lproj of int * Projection.Repr.t * lambda
+ | Lproj of Projection.Repr.t * lambda
| Luint of uint
(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation