aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorMichael Soegtrop2020-03-03 14:37:24 +0100
committerMichael Soegtrop2020-03-03 15:05:54 +0100
commit9168e0e23142ccafbe8b6272551dbb739f72ae95 (patch)
treeea06db07be5371dc4116cf833a0543e7d830abf1 /doc
parent18aa9ca60ec9b3d1712276ec0c615dfe54c1a251 (diff)
Ltac2: Add notation for enough and eenough
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/05-tactic-language/11740-ltac2-enough.rst4
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/05-tactic-language/11740-ltac2-enough.rst b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst
new file mode 100644
index 0000000000..ced3e0ab60
--- /dev/null
+++ b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst
@@ -0,0 +1,4 @@
+- **Added:**
+ Ltac2 notations for enough an eenough
+ (`#11740 <https://github.com/coq/coq/pull/11740>`_,
+ by Michael Soegtrop).