diff options
Diffstat (limited to 'cfrontend/Cminorgen.v')
-rw-r--r-- | cfrontend/Cminorgen.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 8ecf4989..ae6ec56b 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. |