The Coq mailing list

[Sunil Kothari <skothari AT uwyo.edu>]

Thanks Pierre. Appreciate it.
Sunil
________________________________________
From: 
pierre.courtieu AT gmail.com
 
[pierre.courtieu AT gmail.com]
 On Behalf Of Pierre Courtieu 
[Pierre.Courtieu AT cnam.fr]
Sent: Wednesday, October 21, 2009 3:29 AM
To: Sunil Kothari
Cc: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Functional Induction tactic being experimental

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<mailto: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