From 4f507fa565a43b419af6ea7a641a353f62213b21 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 11:40:47 +0200
Subject: Remove the warning for loops

---
 compiler/Driver.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'compiler/Driver.ml')

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
-- 
cgit v1.2.3