Granting #3717 (more informative error message on missing arguments for functional induction).

1 files changed, 9 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8e95f742e4..599d42ee49 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3804,7 +3804,15 @@ let induction_without_atomization isrec with_evars elim names lid =
   in
   let nlid = List.length lid in
   if not (Int.equal nlid awaited_nargs)
-  then Tacticals.New.tclZEROMSG (str"Not the right number of induction arguments.")
+  then Tacticals.New.tclZEROMSG
+    (str"Not the right number of induction arguments (expected "
+     ++ pr_enum (fun x -> x)
+       [
+        if scheme.farg_in_concl then str "the function name" else mt();
+        if scheme.nparams != 0 then int scheme.nparams ++ str (String.plural scheme.nparams " parameter") else mt ();
+        if scheme.nargs != 0 then int scheme.nargs ++ str (String.plural scheme.nargs " argument") else mt ();
+        if Option.is_empty scheme.indarg then mt () else str "a dependent call"  (* ?? *)]
+         ++ str ").")
   else
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
       (induction_from_context_l with_evars elim_info lid names)