diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 200c52efc1..9873d2d5a3 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -432,7 +432,7 @@ TACTIC EXTEND fauto [ "fauto" tactic(tac)] -> [ let heuristic = chose_heuristic None in - finduction None heuristic (snd tac) + finduction None heuristic (Tacinterp.eval_tactic tac) ] | [ "fauto" ] -> |