diff options
author | Julien Forest <forest@ensiie.fr> | 2018-04-09 11:20:24 +0200 |
---|---|---|
committer | Julien Forest <julien.forest@ensiie.fr> | 2018-04-11 14:59:25 +0200 |
commit | 8bb827fd5b979abe17525a6f0256cadb64dd0a23 (patch) | |
tree | 74f6a9668fdf5794bdb6c88d4df96364bf070c21 /plugins/funind | |
parent | 8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff) |
Correction of ugly message described in #4667
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/indfun.ml | 15 |
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 = |