aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/funind/indfun.ml15
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 =