diff options
Diffstat (limited to 'backend/Cmconstr.v')
| -rw-r--r-- | backend/Cmconstr.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Cmconstr.v b/backend/Cmconstr.v index cd50e38e..da642f8f 100644 --- a/backend/Cmconstr.v +++ b/backend/Cmconstr.v @@ -907,5 +907,5 @@ Definition store (chunk: memory_chunk) (e1 e2: expr) := (** ** If-then-else statement *) -Definition ifthenelse (e: expr) (ifso ifnot: stmtlist) : stmt := +Definition ifthenelse (e: expr) (ifso ifnot: stmt) : stmt := Sifthenelse (condexpr_of_expr e) ifso ifnot. |