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.
---
 ...61-functional-induction-throws-unrecoverable-error.rst | 13 +++++++++++++
 plugins/funind/g_indfun.mlg                               | 15 +++++++--------
 test-suite/success/Funind.v                               |  2 +-
 3 files changed, 21 insertions(+), 9 deletions(-)
 create mode 100644 doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst

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).
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 68e1087b74..a1094e39a4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -18,6 +18,7 @@ open Indfun_common
 open Indfun
 open Stdarg
 open Tacarg
+open Extraargs
 open Tactypes
 open Pcoq.Prim
 open Pcoq.Constr
@@ -96,14 +97,12 @@ let functional_induction b c x pat =
 }
 
 TACTIC EXTEND newfunind
-| ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
-     {
-       let c = match cl with
-         | [] -> assert false
-         | [c] -> c
-         | c::cl -> EConstr.applist(c,cl)
-       in
-       Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl }
+| ["functional" "induction" lconstr(c) fun_ind_using(princl) with_names(pat)] ->
+   {
+     (Extratactics.onSomeWithHoles
+          (fun x -> functional_induction true c x pat) princl)
+   }
+
 END
 (***** debug only ***)
 TACTIC EXTEND snewfunind
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index f87f2e2a9d..e371cf251f 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -77,7 +77,7 @@ Functional Scheme app_ind := Induction for app Sort Prop.
 
 Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'.
 intros A l l'.
- functional induction app A l l';  intuition.
+ functional induction app l l';  intuition.
  rewrite <- H0; trivial.
 Qed.
 
-- 
cgit v1.2.3


From e83a92d8855f1b2f99f2960454898985593d4cb6 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 16 May 2020 15:41:21 +0200
Subject: Fix note on implicit arguments in doc of functional induction.

---
 doc/sphinx/using/libraries/funind.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index 40f9eedcf0..3625eac4a5 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -190,9 +190,9 @@ Tactics
 
    .. note::
       :n:`(@qualid {+ @term})` must be a correct full application
-         of :n:`@qualid`. In particular, the rules for implicit arguments are the
-         same as usual. For example use :n:`@qualid` if you want to write implicit
-         arguments explicitly.
+      of :n:`@qualid`. In particular, the rules for implicit arguments are the
+      same as usual. For example use :n:`@@qualid` if you want to write implicit
+      arguments explicitly.
 
    .. note::
       Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped.
-- 
cgit v1.2.3