diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3f728ddcd..70a892a3b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -26,8 +26,8 @@ let is_rec_info scheme_info = let choose_dest_or_ind scheme_info = if is_rec_info scheme_info - then Tactics.new_induct false - else Tactics.new_destruct false + then Tactics.induction false + else Tactics.destruct false let functional_induction with_clean c princl pat = Dumpglob.pause (); |