From 8bb827fd5b979abe17525a6f0256cadb64dd0a23 Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Mon, 9 Apr 2018 11:20:24 +0200 Subject: Correction of ugly message described in #4667 --- plugins/funind/indfun.ml | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'plugins/funind') 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 = -- cgit v1.2.3