diff options
| author | Emilio Jesus Gallego Arias | 2020-02-13 15:35:21 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-13 15:35:21 +0100 |
| commit | eb83c142eb33de18e3bfdd7c32ecfb797a640c38 (patch) | |
| tree | 279ecfcf59459e2601e88e911995d021f88c74b6 /doc/changelog | |
| parent | e76b9da873d2e690e9dd24ed36ecec505676651e (diff) | |
| parent | 7ff035754c1b728ea0314c60d963ba3505898fe5 (diff) | |
Merge PR #11098: Let Arguments support anonymous implicit arguments
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst new file mode 100644 index 0000000000..32526babdb --- /dev/null +++ b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst @@ -0,0 +1,8 @@ +- **Added:** + :cmd:`Arguments <Arguments (implicits)>` now supports setting + implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`. + (`#11098 <https://github.com/coq/coq/pull/11098>`_, + by Hugo Herbelin, fixes `#4696 + <https://github.com/coq/coq/pull/4696>`_, `#5173 + <https://github.com/coq/coq/pull/5173>`_, `#9098 + <https://github.com/coq/coq/pull/9098>`_.). |