From 6f98b3b5f730d66f1878941d780db7b4384fbf60 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 12 Jun 2020 12:04:44 +0100
Subject: Always try inlining functions

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

diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml
index 2e83eb0c..a2570da5 100644
--- a/backend/Inliningaux.ml
+++ b/backend/Inliningaux.ml
@@ -87,9 +87,6 @@ let static_called_once id io =
 
 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
+    true
   end else
     false
-- 
cgit