From 77ce8ba291afa9f5629a160df440f9af6614f3ef Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 27 Jul 2020 09:54:00 +0200
Subject: Add __builtin_sqrt as synonymous for __builtin_fsqrt

__builtin_sqrt (no "f") is the name used by GCC and Clang.
---
 x86/Asmexpand.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'x86')

diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index e4cf028f..caa9775a 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -378,7 +378,7 @@ let expand_builtin_inline name args res =
      emit (Paddl_ri(res, coqint_of_camlint 32l));
      emit (Plabel lbl2)
   (* Float arithmetic *)
-  | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) ->
+  | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) ->
      emit (Psqrtsd (res,a1))
   | "__builtin_fmax", [BA(FR a1); BA(FR a2)], BR(FR res) ->
      if res = a1 then
-- 
cgit