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.
---
 plugins/funind/g_indfun.mlg | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3