fix & update

h0nzZik · Jan 22, 2024 · 70f9207 · 70f9207
1 parent 83e5f2c
commit 70f9207
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 8 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/minuska/theories/BuiltinValue.v b/minuska/theories/BuiltinValue.v
@@ -1188,10 +1188,7 @@ Section sec.
             {
                 destruct a; unfold bv_to_tree; fold bv_to_tree.
                 {
-                    ltac1:(simp BVsize in Hr).
-                    ltac1:(simp BVsize in IHm).
-                    ltac1:(specialize (IHm ltac:(lia))).
-                    unfold my_list_size in Hr.
+                    ltac1:(specialize (IHm ltac:(simpl in *; lia))).
                     simpl in IHm.
                     rewrite bind_Some in IHm.
                     destruct IHm as [x [IHm1 IHm2]].
@@ -1287,7 +1284,7 @@ Section sec.
 
                         ltac1:(ospecialize (IHao2 _)).
                         {
-                            simpl in Hr. ltac1:(lia).
+                            simpl in Hr. ltac1:(simpl in *; lia).
                         }
                         simpl in IHao2.
                         rewrite bind_Some in IHao2.