From 58b59cce492f53ebd9aa960306f07f816c2e279d Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sat, 13 Apr 2019 15:58:38 +0200
Subject: Add a built-in function for "select" (strict conditional)

The built-in is called `EF_select` and has type `(int, T, T) -> T` for
a given Cminor type T.

During instruction selection, it is turned into an `Osel` operation if
available, otherwise into an if/then/else.
---
 exportclight/ExportClight.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'exportclight/ExportClight.ml')

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index b124586a..05cbed71 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -269,6 +269,8 @@ let external_function p = function
               coqstring text
               signatur sg
               (print_list coqstring) clob
+  | EF_select ty ->
+      fprintf p "@[<hov 2>(EF_select %a)@]" asttype ty
 
 (* Expressions *)
 
-- 
cgit