From a5ffc59246b09a389e5f8cbc2f217e323e76990f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 13 Jun 2011 18:11:19 +0000
Subject: Revised handling of annotation statements, and more generally
 built-in functions, and more generally external functions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Machtyping.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'backend/Machtyping.v')

diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 95ceafe..2d8c83d 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -77,6 +77,10 @@ Inductive wt_instr : instruction -> Prop :=
       List.map mreg_type args = (ef_sig ef).(sig_args) ->
       mreg_type res = proj_sig_res (ef_sig ef) ->
       wt_instr (Mbuiltin ef args res)
+  | wt_Mannot:
+      forall ef args,
+      ef_reloads ef = false ->
+      wt_instr (Mannot ef args)
   | wt_Mgoto:
       forall lbl,
       wt_instr (Mgoto lbl)
-- 
cgit v1.2.3