summaryrefslogtreecommitdiff
path: root/cfrontend/Cminorgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cminorgen.v')
-rw-r--r--cfrontend/Cminorgen.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 8ecf498..ae6ec56 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -70,6 +70,8 @@ Definition transl_constant (cst: Csharpminor.constant): constant :=
Ointconst n
| Csharpminor.Ofloatconst n =>
Ofloatconst n
+ | Csharpminor.Osingleconst n =>
+ Osingleconst n
| Csharpminor.Olongconst n =>
Olongconst n
end.