diff options
| author | Hugo Herbelin | 2020-02-02 23:28:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-11 16:18:59 +0100 |
| commit | cd5bb3c76e430392e4363dc7b4b5bbe0cafa466f (patch) | |
| tree | b650dfc7f9dea29afc7e0645dd9c0220fff03439 | |
| parent | 6975536db325a0f4dcbcb609dd8959d45fc19830 (diff) | |
Lately adding a changelog for PR#10202.
| -rw-r--r-- | doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst new file mode 100644 index 0000000000..57bce7e4f6 --- /dev/null +++ b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst @@ -0,0 +1,7 @@ +- **Changed:** + Warn when manual implicit arguments are used in unexpected positions + of a term (e.g. in `Check id (forall {x}, x)`) or when a implicit + argument name is shadowed (e.g. in `Check fun f : forall {x:nat} + {x}, nat => f`) + (`#10202 <https://github.com/coq/coq/pull/10202>`_, + by Hugo Herbelin). |