remove "Fail Timeout"s to make Windows happy (#447)

mit-plv · Feb 12, 2025 · d0bb7a7 · d0bb7a7
1 parent dca97a1
commit d0bb7a7
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/bedrock2/src/bedrock2Examples/kyberslash.v b/bedrock2/src/bedrock2Examples/kyberslash.v
@@ -269,13 +269,12 @@ Section WithWord.
                 seprewrite_in (@array_index_nat_inbounds _ _ _ _ _ _ _ scalar16 (word.of_Z 2) (word.of_Z 0) x5 x8 (Z.to_nat (word.unsigned n))) H11.
                 2: { repeat straightline. use_sep_assumption. cancel.
                      cancel_seps_at_indices 1%nat 0%nat.
-                     { f_equal. f_equal. subst v1 n. Fail Timeout 1 ZnWords.
+                     { f_equal. f_equal. subst v1 n.
                        rewrite Z2Nat.id.
                        2: { assert (Hnonneg:= word.unsigned_range (word.add (word.mul v2 x1) x6)).
                             blia. }
                        ZnWords. }
                      ecancel_done. }
-                Fail Timeout 1 ZnWords.
                 subst. subst v1. subst v0. subst v2.
                 assert (Hnonneg := word.unsigned_range (word.add (word.mul (word.of_Z 8) x1) x6)).
                 enough ((word.unsigned (word.add (word.mul (word.of_Z 8) x1) x6)) < KYBER_N).