summaryrefslogtreecommitdiff
path: root/extraction/extraction.v
diff options
context:
space:
mode:
Diffstat (limited to 'extraction/extraction.v')
-rw-r--r--extraction/extraction.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index fc2920e..abb792c 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -30,6 +30,7 @@ Extract Constant Floats.Float.neg => "( ~-. )".
Extract Constant Floats.Float.abs => "abs_float".
Extract Constant Floats.Float.singleoffloat => "Floataux.singleoffloat".
Extract Constant Floats.Float.intoffloat => "Floataux.intoffloat".
+Extract Constant Floats.Float.intuoffloat => "Floataux.intuoffloat".
Extract Constant Floats.Float.floatofint => "Floataux.floatofint".
Extract Constant Floats.Float.floatofintu => "Floataux.floatofintu".
Extract Constant Floats.Float.add => "( +. )".