diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-08 17:40:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-08 20:44:29 +0200 |
| commit | f87c3a55b1ad52b63ebd0af0cf9f3fb0e8e86f76 (patch) | |
| tree | 348006f1c5abfed0a69e67f3090e479a5d26b58a /plugins | |
| parent | 8bbd7ceb554f68f0473f492f45e0f909af15992b (diff) | |
Renaming new_induct -> induction; new_destruct -> destruct.
Diffstat (limited to 'plugins')
| -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 (); |