aboutsummaryrefslogtreecommitdiff
path: root/engine/eConstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.mli')
-rw-r--r--engine/eConstr.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 49cbc4d7e5..2f4cf7d5d0 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -124,10 +124,12 @@ val mkCase : case_info * t * t * t array -> t
val mkFix : (t, t) pfixpoint -> t
val mkCoFix : (t, t) pcofixpoint -> t
val mkArrow : t -> t -> t
+val mkInt : Uint63.t -> t
val mkRef : GlobRef.t * EInstance.t -> t
val applist : t * t list -> t
+val applistc : t -> t list -> t
val mkProd_or_LetIn : rel_declaration -> t -> t
val mkLambda_or_LetIn : rel_declaration -> t -> t