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.

3 files changed, 21 insertions, 9 deletions

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.