From 9c72ffe762dc2f90109d5991f74ee0ee4e9a8ec3 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 13 Mar 2022 16:35:30 +0000
Subject: Add always inlining

---
 backend/Inliningaux.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml
index cf308962..0607547b 100644
--- a/backend/Inliningaux.ml
+++ b/backend/Inliningaux.ml
@@ -90,9 +90,6 @@ let small_enough (f : coq_function) =
 
 let should_inline (io: inlining_info) (id: ident) (f: coq_function) =
   if !Clflags.option_finline then begin
-    match C2C.atom_inline id with
-    | C2C.Inline -> true
-    | C2C.Noinline -> false
-    | C2C.No_specifier -> static_called_once id io || small_enough f
+    true
   end else
     false
-- 
cgit