diff options
Diffstat (limited to 'cfrontend/Csyntax.v')
| -rw-r--r-- | cfrontend/Csyntax.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 48c326e..c82aa9e 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -108,7 +108,8 @@ with fieldlist : Type := Inductive unary_operation : Type := | Onotbool : unary_operation (**r boolean negation ([!] in C) *) | Onotint : unary_operation (**r integer complement ([~] in C) *) - | Oneg : unary_operation. (**r opposite (unary [-]) *) + | Oneg : unary_operation (**r opposite (unary [-]) *) + | Ofabs : unary_operation. (**r floating-point absolute value *) Inductive binary_operation : Type := | Oadd : binary_operation (**r addition (binary [+]) *) |