Skip to content

Commit

Permalink
remove unnecessary parentheses
Browse files Browse the repository at this point in the history
  • Loading branch information
t6s committed Dec 8, 2023
1 parent 30bb2f3 commit c092788
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lib/ssr_ext.v
Original file line number Diff line number Diff line change
Expand Up @@ -704,7 +704,7 @@ Proof.
subst m n => /=.
case => /= tv.
apply eq_from_tnth => i.
rewrite (tnth_nth (t!_i)) [in X in _ = X](tnth_nth (t!_i)).
rewrite (tnth_nth t!_i) [in X in _ = X](tnth_nth t!_i).
by rewrite -(@nth_take k) // -[in X in _ = X](@nth_take k) // tv.
Qed.

Expand Down

0 comments on commit c092788

Please sign in to comment.