summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Driver.ml8
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