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 c8fbb27a9..47d8d9564 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -138,6 +138,7 @@ type fv_elem =
FVnamed of Id.t
| FVrel of int
| FVuniv_var of int
+| FVevar of Evar.t
type fv = fv_elem array