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