diff options
Diffstat (limited to 'doc/changelog')
3 files changed, 23 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/13965-syndef-principal-scope.rst b/doc/changelog/03-notations/13965-syndef-principal-scope.rst new file mode 100644 index 0000000000..448dbbe3c7 --- /dev/null +++ b/doc/changelog/03-notations/13965-syndef-principal-scope.rst @@ -0,0 +1,12 @@ +- **Added:** + Let the user specify a scope for abbreviation arguments, e.g. + ``Notation abbr X := t (X in scope my_scope)``. + (`#13965 <https://github.com/coq/coq/pull/13965>`_, + by Enrico Tassi). +- **Changed:** + The error ``Argument X was previously inferred to be in scope + XXX_scope but is here used in YYY_scope.`` is now the warning + ``[inconsistent-scopes,syntax]`` and can be silenced by + specifying the scope of the argument + (`#13965 <https://github.com/coq/coq/pull/13965>`_, + by Enrico Tassi). diff --git a/doc/changelog/05-tactic-language/14128-ltac2-bool-equal-rename.rst b/doc/changelog/05-tactic-language/14128-ltac2-bool-equal-rename.rst new file mode 100644 index 0000000000..17eb710344 --- /dev/null +++ b/doc/changelog/05-tactic-language/14128-ltac2-bool-equal-rename.rst @@ -0,0 +1,5 @@ +- **Changed:** + Renamed Ltac2 Bool.eq into Bool.equal for uniformity. + The old function is now a deprecated alias + (`#14128 <https://github.com/coq/coq/pull/14128>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/12-misc/14041-cs_lambda.rst b/doc/changelog/12-misc/14041-cs_lambda.rst new file mode 100644 index 0000000000..872b1f09eb --- /dev/null +++ b/doc/changelog/12-misc/14041-cs_lambda.rst @@ -0,0 +1,6 @@ +- **Added:** + Enable canonical `fun _ => _` projections, + see :ref:`canonicalstructures` for details. + (`#14041 <https://github.com/coq/coq/pull/14041>`_, + by Jan-Oliver Kaiser and Pierre Roux, + reviewed by Cyril Cohen and Enrico Tassi). |