From 701b51a882defa39ecfc292f40d4e7e5b7f9548a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Apr 2017 16:27:55 -0700 Subject: [PATCH] chore(library/tools/mini_crush/default): increase timeout --- library/tools/mini_crush/default.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/tools/mini_crush/default.lean b/library/tools/mini_crush/default.lean index 64c2fccf68..9b02218962 100644 --- a/library/tools/mini_crush/default.lean +++ b/library/tools/mini_crush/default.lean @@ -113,7 +113,7 @@ when_tracing `mini_crush $ /- Simple tactic -/ meta def close_aux (hs : hinst_lemmas) : tactic unit := triv <|> reflexivity reducible <|> contradiction -<|> try_for 100 (rsimp {} hs >> now) <|> try_for 100 reflexivity +<|> try_for 1000 (rsimp {} hs >> now) <|> try_for 1000 reflexivity meta def close (hs : hinst_lemmas) (s : name) (e : option expr) : tactic unit := now