From d958feb5f30255d3b9ca84bf5be89c299ddb8a5f Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 18 Jun 2020 20:12:36 +0200
Subject: Fix #12228 negative integers not accepted in ltac integer_list

---
 doc/changelog/05-tactic-language/12541-fix12228.rst | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/05-tactic-language/12541-fix12228.rst

(limited to 'doc')

diff --git a/doc/changelog/05-tactic-language/12541-fix12228.rst b/doc/changelog/05-tactic-language/12541-fix12228.rst
new file mode 100644
index 0000000000..286760e008
--- /dev/null
+++ b/doc/changelog/05-tactic-language/12541-fix12228.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Excluding occurrences was causing an anomaly in tactics
+  (e.g., :g:`pattern _ at L` where :g:`L` is :g:`-2`).
+  (`#12541 <https://github.com/coq/coq/pull/12541>`_,
+  fixes `#12228 <https://github.com/coq/coq/issues/12228>`_,
+  by Pierre Roux).
-- 
cgit v1.2.3