blob: 3dd103b115e26a087dfc5adb12e9da59f2e5f604 (
plain)
1
2
3
4
5
6
|
- **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).
|
