Merge PR #7202: Correction of ugly message described in #4667

1 files changed, 12 insertions, 3 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9c350483b..d395e3601 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -91,10 +91,19 @@ let functional_induction with_clean c princl pat =
 	if princ_infos.Tactics.farg_in_concl
 	then [c] else []
       in
+      if List.length args + List.length c_list = 0
+      then user_err Pp.(str "Cannot recognize a valid functional scheme" );
       let encoded_pat_as_patlist =
-        List.make (List.length args + List.length c_list - 1) None @ [pat] in
-      List.map2 (fun c pat -> ((None,Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None))
-        (args@c_list) encoded_pat_as_patlist
+        List.make (List.length args + List.length c_list - 1) None @ [pat]
+      in
+      List.map2
+        (fun c pat ->
+          ((None,
+            Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))),
+           (None,pat),
+           None))
+        (args@c_list)
+        encoded_pat_as_patlist
     in
     let princ' = Some (princ,bindings) in
     let princ_vars =