From 54dea0fc061f5daee5976450ec84ddb7e15c5db9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 11 Feb 2022 11:12:45 +0100 Subject: remove singleoflongu (does not exist) --- kvx/SelectOpproof.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'kvx/SelectOpproof.v') diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index 658bf0b3..e6cce0fa 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1929,6 +1929,28 @@ Proof. } inv EVAL. constructor. + - cbn in *. + intro EVAL. + inv EVAL. discriminate. + inv H0. discriminate. + inv H2. 2: discriminate. + inv Heval. + intro EVAL. + destruct v1; try discriminate. + destruct v0; try discriminate. + unfold Int64.eq in EVAL. + change (Int64.unsigned Int64.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vlong (Int64.divu i i0)). split. + { + apply FPDivision64.fp_divu64_correct; auto. + pose proof (Int64.unsigned_range i0). + lia. + } + inv EVAL. + constructor. Qed. End CMCONSTR. -- cgit