diff options
Diffstat (limited to 'src/Compilers/Z/Syntax/Util.v')
-rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index 9f18f47e9..b84a00dee 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -61,6 +61,9 @@ Definition genericize_op {var' src dst} (opc : op src dst) {f} | Land _ _ _ => fun _ _ => Land _ _ _ | Lor _ _ _ => fun _ _ => Lor _ _ _ | Opp _ _ => fun _ _ => Opp _ _ + | Zselect _ _ _ _ => fun _ _ => Zselect _ _ _ _ + | AddWithCarry _ _ _ _ => fun _ _ => AddWithCarry _ _ _ _ + | AddWithGetCarry bitwidth _ _ _ _ _ => fun _ _ => AddWithGetCarry bitwidth _ _ _ _ _ end. Lemma cast_const_id {t} v |