diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Driver.ml | 12 |
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 |