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 cd1de4c834..720f11b8f2 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -115,6 +115,7 @@ type fterm = | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FInt of Uint63.t + | FFloat of Float64.t | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED |