From 7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 2 Jan 2021 21:22:07 -0800 Subject: [PATCH] Use auto instead of apply. --- day8.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/day8.v b/day8.v index 7ce4669..1212d5f 100644 --- a/day8.v +++ b/day8.v @@ -235,9 +235,9 @@ Module DayEight (Import M:Int). intros pc acc. destruct (valid_input_progress pc l acc) as [[_ Hd]|[pc' [Hw [[_ Hst]|[pc'' [acc'' [Hin Hst]]]]]]]. - (* We're done. *) - eexists. apply run_noswap_ok. apply Hd. + eexists. apply run_noswap_ok. assumption. - (* We're stuck. *) - eexists. apply run_noswap_fail. apply Hst. + eexists. apply run_noswap_fail. assumption. - (* We can make a step. This will remove our current PC from the valid list, *) edestruct (H (set_remove Fin.eq_dec pc' l)). (* Since the PC must be in the list, removing it makes the list smaller. *)