diff options
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 6f5afc4e27..e755f28d98 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -134,7 +134,7 @@ val create: one by one *) type 'a stack_member = - | Zapp of 'a array * int + | Zapp of 'a list | Zcase of case_info * 'a * 'a array | Zfix of 'a * 'a stack | Zshift of int @@ -182,6 +182,7 @@ type fterm = | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs + | FLOCKED and freference = | FConst of section_path * fconstr array |