summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Driver.ml12
1 files changed, 12 insertions, 0 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index e0504903..e7425122 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -199,6 +199,18 @@ let () =
in
if has_loops then log#lwarning (lazy "Support for loops is experimental");
+ (* If we target Lean, we request the crates to be split into several files
+ whenever there are opaque functions *)
+ if
+ !backend = Lean
+ && List.exists (fun (d : A.fun_decl) -> d.body = None) m.functions
+ && not !split_files
+ then (
+ log#error
+ "For Lean, we request the -split-file option whenever using opaque \
+ functions";
+ fail ());
+
(* Apply the pre-passes *)
let m = PrePasses.apply_passes m in