aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cbytecodes.mli')
-rw-r--r--kernel/cbytecodes.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 71dd65186..11e07c00e 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -137,6 +137,7 @@ type fv_elem =
FVnamed of Id.t
| FVrel of int
| FVuniv_var of int
+| FVevar of Evar.t
type fv = fv_elem array