summaryrefslogtreecommitdiff
path: root/cfrontend/Cminorgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cminorgen.v')
-rw-r--r--cfrontend/Cminorgen.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 27aa453..34a1080 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -50,6 +50,7 @@ Definition make_op (op: Csharpminor.operation) (el: exprlist): option expr :=
| Csharpminor.Ocast16unsigned => Some(Cmconstr.cast16unsigned e1)
| Csharpminor.Ocast16signed => Some(Cmconstr.cast16signed e1)
| Csharpminor.Onotint => Some(Cmconstr.notint e1)
+ | Csharpminor.Onotbool => Some(Cmconstr.notbool e1)
| Csharpminor.Onegf => Some(Cmconstr.negfloat e1)
| Csharpminor.Oabsf => Some(Cmconstr.absfloat e1)
| Csharpminor.Osingleoffloat => Some(Cmconstr.singleoffloat e1)