aboutsummaryrefslogtreecommitdiff
path: root/engine/eConstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.mli')
-rw-r--r--engine/eConstr.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2afce38db7..90f50b764c 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -127,6 +127,7 @@ val mkCoFix : (t, t) pcofixpoint -> t
val mkArrow : t -> Sorts.relevance -> t -> t
val mkArrowR : t -> t -> t
val mkInt : Uint63.t -> t
+val mkFloat : Float64.t -> t
val mkRef : GlobRef.t * EInstance.t -> t