summaryrefslogtreecommitdiff
path: root/src/monomorphise.mli
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-07-16 18:57:46 +0100
committerAlasdair Armstrong2019-07-16 18:57:46 +0100
commitcd909e15b97739b10214023af04b2fbbb4d20cf7 (patch)
tree9a418c7cafa915c29e93242848a1411cbd8b8f7c /src/monomorphise.mli
parent6d3a6edcd616621eb40420cfb16a34762a32c5c1 (diff)
parent170543faa031d90186e6b45612ed8374f1c25f7b (diff)
Merge remote-tracking branch 'origin/sail2' into separate_bv
Diffstat (limited to 'src/monomorphise.mli')
-rw-r--r--src/monomorphise.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/monomorphise.mli b/src/monomorphise.mli
index 1a82c8d0..39d89461 100644
--- a/src/monomorphise.mli
+++ b/src/monomorphise.mli
@@ -56,6 +56,7 @@ type options = {
}
val monomorphise :
+ string -> (* Target backend *)
options ->
((string * int) * string) list -> (* List of splits from the command line *)
Type_check.tannot Ast.defs ->