From 222031f6edc934ff4611a46780a148e1160c1d7b Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Wed, 26 May 2021 18:47:52 +0200
Subject: Minor changes on the Coq part

---
 src/bva/BVList.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/bva/BVList.v')

diff --git a/src/bva/BVList.v b/src/bva/BVList.v
index 91a110d..9e22f98 100644
--- a/src/bva/BVList.v
+++ b/src/bva/BVList.v
@@ -589,7 +589,7 @@ Definition ult_list (x y: list bool) :=
   (ult_list_big_endian (List.rev x) (List.rev y)).
 
 
-Fixpoint slt_list_big_endian (x y: list bool) :=
+Definition slt_list_big_endian (x y: list bool) :=
   match x, y with
     | nil, _  => false
     | _ , nil => false
@@ -2103,7 +2103,7 @@ Proof. intro a.
        induction a as [ | xa xsa IHa ].
        - intros. simpl. easy.
        - intros.
-         case b in *. simpl. rewrite IHa. simpl. omega.
+         case b in *. simpl. rewrite IHa. simpl. lia.
          simpl. case (k - 1 <? 0)%Z; simpl; now rewrite IHa.
 Qed. 
 
@@ -2117,8 +2117,8 @@ Lemma prop_mult_bool_step: forall k' a b res k,
                        length (mult_bool_step a b res k k') = (length res)%nat.
 Proof. intro k'.
        induction k'.
-       - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. omega.
-       - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; omega.
+       - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. lia.
+       - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; lia.
 Qed.
 
 Lemma and_with_bool_len: forall a b, length (and_with_bool a (nth 0 b false)) = length a.
-- 
cgit