From b3208d9a581e7575c41d545964f4f85c6f3b4d66 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Tue, 7 Jul 2020 13:24:59 +0100 Subject: Get Coqup compiling again on dev-nadesh. --- src/translation/HTLgen.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/translation/HTLgen.v') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 32b6e04..babbc01 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -275,8 +275,8 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : | Op.Ccompu c, _ => translate_comparison c args | Op.Ccompimm c i, _ => translate_comparison_imm c args i | Op.Ccompuimm c i, _ => translate_comparison_imm c args i - | Op.Cmaskzero n, r::nil => ret (Vbinop Veq (boplit Vand r n) (Vlit (ZToValue 32 0))) - | Op.Cmasknotzero n, r::nil => ret (Vbinop Vne (boplit Vand r n) (Vlit (ZToValue 32 0))) + | Op.Cmaskzero n, r::nil => ret (Vbinop Veq (boplit Vand r n) (Vlit (ZToValue 0))) + | Op.Cmasknotzero n, r::nil => ret (Vbinop Vne (boplit Vand r n) (Vlit (ZToValue 0))) | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") end. -- cgit