From 478ae4c3aeb1a31b0eec9ab7eb8fe20ec2671614 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sun, 6 Mar 2016 10:36:55 +0100
Subject: Misc updates following the introduction of the new linking framework

---
 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 5d4ab88b..b5877f8b 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -237,6 +237,8 @@ let external_function p = function
       fprintf p "@[<hov 2>(EF_external %a@ %a)@]" coqstring name signatur sg
   | EF_builtin(name, sg) ->
       fprintf p "@[<hov 2>(EF_builtin %a@ %a)@]" coqstring name signatur sg
+  | EF_runtime(name, sg) ->
+      fprintf p "@[<hov 2>(EF_runtime %a@ %a)@]" coqstring name signatur sg
   | EF_vload chunk ->
       fprintf p "(EF_vload %s)" (name_of_chunk chunk)
   | EF_vstore chunk ->
-- 
cgit