diff options
author | Son Ho | 2023-10-25 11:40:47 +0200 |
---|---|---|
committer | Son Ho | 2023-10-25 11:40:47 +0200 |
commit | 4f507fa565a43b419af6ea7a641a353f62213b21 (patch) | |
tree | 1c7d4e22b12fd3b4f5c8fa26ccf93c9de8acf485 /compiler | |
parent | ece74df70f12790bab7ecfe0c590c2c637e89801 (diff) |
Remove the warning for loops
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/Driver.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 414b042d..3b9ea4d1 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -214,14 +214,6 @@ let () = log#linfo (lazy ("Imported: " ^ filename)); log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")); - (* Print a warning if the crate contains loops (loops are experimental for now) *) - let has_loops = - 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"); - (* We don't support mutually recursive definitions with decreases clauses in Lean *) if !backend = Lean && !extract_decreases_clauses |