diff options
author | Son Ho | 2023-08-08 17:42:30 +0200 |
---|---|---|
committer | Son Ho | 2023-08-08 17:42:30 +0200 |
commit | 6cdbb77f2be6f349729e2fd075ca3c51e9365b4f (patch) | |
tree | 4177ec5e62c739d22dd0e6ea69fdd942df691998 /compiler/Driver.ml | |
parent | 1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (diff) |
Update the code following a refactor on Charon's side
Diffstat (limited to '')
-rw-r--r-- | compiler/Driver.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index d819768b..b646a53d 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -214,7 +214,9 @@ let () = (* Print a warning if the crate contains loops (loops are experimental for now) *) let has_loops = - List.exists Aeneas.LlbcAstUtils.fun_decl_has_loops m.functions + A.FunDeclId.Map.exists + (fun _ -> Aeneas.LlbcAstUtils.fun_decl_has_loops) + m.functions in if has_loops then log#lwarning (lazy "Support for loops is experimental"); @@ -222,7 +224,9 @@ let () = whenever there are opaque functions *) if !backend = Lean - && List.exists (fun (d : A.fun_decl) -> d.body = None) m.functions + && A.FunDeclId.Map.exists + (fun _ (d : A.fun_decl) -> d.body = None) + m.functions && not !split_files then ( log#error |