The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Function and functional induction are marked as experimental because it may be reimplemented in the next two years. However its semantic should not change much in the case that it already deals with. In this sense we could have removed the word "experimental" from the documentation. You can use it with no worry.  I encourage you to do so and to report bugs/needs.

However this feature has some limitations, mainly on dependently typed functions, that we hope to work on during the next months/years. In this sense this feature is still in development.

Hope this helps, 
Pierre Courtieu

2009/10/20 Sunil Kothari <skothari AT uwyo.edu>

Hi,

Could some one explain why the Coq manual  (v 8.2 and earlier) describes the functional induction tactic as "experimental" ?  I would appreciate any  papers/pointers  at the issues involved in using this tactic.

Thanks,
Sunil

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club