coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Functional Induction tactic being experimental

From: Sunil Kothari <skothari AT uwyo.edu>
To: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] Functional Induction tactic being experimental
Date: Tue, 20 Oct 2009 10:16:33 -0600
Accept-language: en-US
Acceptlanguage: en-US
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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

[Coq-Club] Functional Induction tactic being experimental, Sunil Kothari
- Re: [Coq-Club] Functional Induction tactic being experimental, Pierre Courtieu
  - RE: [Coq-Club] Functional Induction tactic being experimental, Sunil Kothari