diff options
Diffstat (limited to 'src/Compilers/Z/Syntax/Util.v')
| -rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index daf3d65be..2338efc48 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -71,6 +71,8 @@ Definition genericize_op {var' src dst} (opc : op src dst) {f} | Zselect _ _ _ _ => fun _ _ => Zselect _ _ _ _ | AddWithCarry _ _ _ _ => fun _ _ => AddWithCarry _ _ _ _ | AddWithGetCarry bitwidth _ _ _ _ _ => fun _ _ => AddWithGetCarry bitwidth _ _ _ _ _ + | SubWithBorrow _ _ _ _ => fun _ _ => SubWithBorrow _ _ _ _ + | SubWithGetBorrow bitwidth _ _ _ _ _ => fun _ _ => SubWithGetBorrow bitwidth _ _ _ _ _ end. Lemma cast_const_id {t} v |