- **Added:**
  Syntax :n:`pose proof (@ident:=@term)` as an
  alternative to :n:`pose proof @term as @ident`, following the model of
  :n:`pose (@ident:=@term)`. See documentation of :tacn:`pose proof`
  (`#11522 <https://github.com/coq/coq/pull/11522>`_,
  by Hugo Herbelin).