Merge pull request #1 from fdupress/alt-ergo-2.5

bump alt-ergo up to 2.5
MM45 · Sep 25, 2024 · d5a5b36 · d5a5b36
2 parents 59a4468 + bfa18a5
commit d5a5b36
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 5 deletions.
diff --git a/easycrypt.project b/easycrypt.project
@@ -1,5 +1,5 @@
 [general]
 timeout = 10
-provers = Alt-Ergo@2.4
+provers = Alt-Ergo@2.5
 provers = [email protected]
-provers = [email protected]
+provers = [email protected]
diff --git a/proofs/acai/FL_XMSS_TW.ec b/proofs/acai/FL_XMSS_TW.ec
@@ -220,8 +220,9 @@ proof. smt(list2tree_ok). qed.
 lemma list2tree1 (x : 'a) :
   list2tree [x] = Leaf x.
 proof.
-move: (list2tree_lvb [x] 0 0 _) => //.
-by rewrite expr0 /= int2bs0s /#.
+move: (list2tree_lvb [x] 0 0 _)=> //.
+rewrite expr0 /= int2bs0s rev_nil.
+by case: (list2tree [x]).
 qed.
 
 lemma list2tree_uniq2 ['a] (e : int) (s : 'a list) (t1 t2 : 'a bintree) :

diff --git a/proofs/fsai/FL_XMSS_TW.ec b/proofs/fsai/FL_XMSS_TW.ec
@@ -369,7 +369,8 @@ lemma list2tree1 (x : 'a) :
   list2tree [x] = Leaf x.
 proof.
 move: (list2tree_lvb [x] 0 0 _) => //.
-by rewrite expr0 /= int2bs0s /#.
+rewrite expr0 /= int2bs0s rev_nil.
+by case: (list2tree [x]).
 qed.
 
 lemma list2tree_uniq2 ['a] (e : int) (s : 'a list) (t1 t2 : 'a bintree) :