From 888aaeb0a948352cf56f1f6d8023a051e90583a0 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 14 May 2020 14:46:56 +0200
Subject: Fix #11761: Functional Induction throws unrecoverable error.

Error happened only when writing:

functional induction f x y z.

instead of

functional induction (f x y z).

Now the former is equivalent to the former: implicits must be omitted.
Hence small source of incompatibility, but a more homogeneous
behaviour.
---
 ...1761-functional-induction-throws-unrecoverable-error.rst | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst

(limited to 'doc')

diff --git a/doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst b/doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst
new file mode 100644
index 0000000000..2402321fad
--- /dev/null
+++ b/doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst
@@ -0,0 +1,13 @@
+- **Fixed:**
+  Wrong type error in tactic :tacn:`functional induction`.
+  (`#12326 <https://github.com/coq/coq/pull/12326>`_,
+  by Pierre Courtieu,
+  fixes `#11761 <https://github.com/coq/coq/issues/11761>`_,
+  reported by Lasse Blaauwbroek).
+- **Changed**
+  When the tactic :tacn:`functional induction` :n:`c__1 c__2 ... c__n` is used
+  with no parenthesis around :n:`c__1 c__2 ... c__n`, :n:`c__1 c__2 ... c__n` is now
+  read as one sinlge applicative term. In particular implicit
+  arguments should be omitted. Rare source of incompatibility
+  (`#12326 <https://github.com/coq/coq/pull/12326>`_,
+  by Pierre Courtieu).
-- 
cgit v1.2.3