diff options
Diffstat (limited to 'doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst')
| -rw-r--r-- | doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst deleted file mode 100644 index f10208e9b2..0000000000 --- a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Tactics with qualified name of the form ``Coq.Init.Notations`` are - now qualified with prefix ``Coq.Init.Ltac``; users of the -noinit - option should now import Coq.Init.Ltac if they want to use Ltac - (`#12023 <https://github.com/coq/coq/pull/12023>`_, - by Hugo Herbelin; minor source of incompatibilities). |