diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /engine/eConstr.mli | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 2 |
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 |