From 75fec5716327beb1e93f294b70d563300d8f81ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Mar 2021 16:35:42 +0200
Subject: Properly expand projection parameters in Btermdn.

The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.

We fix this by adding dummy parameter arguments on sight.

Fixes #14009: TC search failure with primitive projections.
---
 doc/changelog/04-tactics/14033-fix-14009.rst | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/04-tactics/14033-fix-14009.rst

(limited to 'doc')

diff --git a/doc/changelog/04-tactics/14033-fix-14009.rst b/doc/changelog/04-tactics/14033-fix-14009.rst
new file mode 100644
index 0000000000..3b58e193cb
--- /dev/null
+++ b/doc/changelog/04-tactics/14033-fix-14009.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Properly expand projection parameters in hint discrimination
+  nets. (`#14033 <https://github.com/coq/coq/pull/14033>`_,
+  fixes `#9000 <https://github.com/coq/coq/issues/9000>`_,
+  `#14009 <https://github.com/coq/coq/issues/14009>`_,
+  by Pierre-Marie Pédrot).
-- 
cgit v1.2.3