aboutsummaryrefslogtreecommitdiffstats
path: root/backend/XTL.mli
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-09-06 22:33:46 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-09-06 22:33:46 +0200
commite64b9464fb6662bf63ac255eca94d17d572c9d81 (patch)
tree517819d4f4e29fbd3a68d6431dd471baf0d427b0 /backend/XTL.mli
parent8e03466a1a2e7bbc9057ac76ee18deda990dc884 (diff)
downloadcompcert-kvx-e64b9464fb6662bf63ac255eca94d17d572c9d81.tar.gz
compcert-kvx-e64b9464fb6662bf63ac255eca94d17d572c9d81.zip
ONE "admitted" and things compile
Diffstat (limited to 'backend/XTL.mli')
-rw-r--r--backend/XTL.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/XTL.mli b/backend/XTL.mli
index 54988d4b..b4b77fab 100644
--- a/backend/XTL.mli
+++ b/backend/XTL.mli
@@ -31,7 +31,7 @@ type instruction =
| Xspill of var * var
| Xparmove of var list * var list * var * var
| Xop of operation * var list * var
- | Xload of memory_chunk * addressing * var list * var
+ | Xload of trapping_mode * memory_chunk * addressing * var list * var
| Xstore of memory_chunk * addressing * var list * var
| Xcall of signature * (var, ident) sum * var list * var list
| Xtailcall of signature * (var, ident) sum * var list