diff options
| author | Hugo Herbelin | 2020-02-04 18:40:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-03 14:21:41 +0100 |
| commit | e559dfc4995ae6777d9ff07d34db738cb77a519c (patch) | |
| tree | 599726a4826154d44aef2cd930f7079cba0eb70b /doc/changelog | |
| parent | ed8ac4195c89ee14d03c80e1d9d3f66665573cbf (diff) | |
Adding an alias "pose proof (x:=a)" for "pose proof a as x".
This is to be consistent with "pose (x:=a)" (and an alternative to
"assert (x:=a)").
This was suggested by
"https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962".
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst new file mode 100644 index 0000000000..579ccf839f --- /dev/null +++ b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst @@ -0,0 +1,6 @@ +- **Added:** + Syntax :tacn:`pose proof (@ident:=@term)` as an + alternative to `pose proof @term as @ident`, following the model of + :tacn:`pose (@ident:=@term)` + (`#11522 <https://github.com/coq/coq/pull/11522>`_, + by Hugo Herbelin). |