Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.

Reviewed-by: ejgallego

4 files changed, 24 insertions, 12 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/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.
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.