diff options
| author | coqbot-app[bot] | 2020-11-16 14:07:25 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 14:07:25 +0000 |
| commit | 1369d1426b0187bb817606966c32fdaf9afe4ed1 (patch) | |
| tree | b032cdae0629912df49aac8d3fee76ec8f3599cc /doc | |
| parent | 89a4b7e7dd82bd46db2d00b6e48b8989d3a5372b (diff) | |
| parent | 5ded9cae169799a51aa713c9f2807d356a37fb58 (diff) | |
Merge PR #13337: Avoid exposing an internal name when "intros _ H" fails because of _ being dependent in H
Reviewed-by: gares
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst b/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst new file mode 100644 index 0000000000..089647a4b2 --- /dev/null +++ b/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Avoiding exposing an internal name of the form :n:`_tmp` when applying the + :n:`_` introduction pattern would break a dependency + (`#13337 <https://github.com/coq/coq/pull/13337>`_, + fixes `#13336 <https://github.com/coq/coq/issues/13336>`_, + by Hugo Herbelin). |