Commit 2022-06-04 17:34 19b57866

feat(tactic/set): fix a bug (#14488) We make the behaviour of tactic.interactive.set closer to that of tactic.interactive.let, this should fix the following issue reported in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/set.20bug.3F/near/284471523:

import ring_theory.adjoin.basic
example {R S : Type*} [comm_ring R] [comm_ring S] [algebra R S] (x : S): false :=
begin
  let y : algebra.adjoin R ({x} : set S) := ⟨x, algebra.self_mem_adjoin_singleton R x⟩, -- works
  set y : algebra.adjoin R ({x} : set S) := ⟨x, algebra.self_mem_adjoin_singleton R x⟩, -- error
  sorry
end

This is related to [lean#555 ](https://github.com/leanprover-community/lean/pull/555) I also fix two completely unrelated docstrings (where the list syntax created two lists instead of one) as I wouldn't want to separately add them to CI...