diff options
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index c1e5f12df7..ada0fc9780 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -118,6 +118,7 @@ type fterm = | FEvar of existential * fconstr subs | FInt of Uint63.t | FFloat of Float64.t + | FArray of Univ.Instance.t * fconstr Parray.t * fconstr | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED |