coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Reset and CoqIde

From: Pierre Boutillier <pierre.boutillier AT ens-lyon.fr>
To: sidi <Sidi.Ould_Biha AT inria.fr>
Cc: Laurent Th�ry <Laurent.Thery AT sophia.inria.fr>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Reset and CoqIde
Date: Thu, 10 Jun 2010 11:26:58 +0200

Le 10 juin 10 � 11:05, sidi a �crit :

Hi Laurent,

Using Navigation does not allow to remove the induction principle
defined by Coq. A solution is to use CoInductive � la SSreflect or PG :)

Regards

Hi,

If you don't want Coq automatic induction principles at all, You can use the "(Un)set Elimination Schemes." command such as it is done in theories/Logic/JMeq.v.

All the best,
Pierre

[Coq-Club] Reset and CoqIde, sidi
- Re: [Coq-Club] Reset and CoqIde, Laurent Théry
  - Re: [Coq-Club] Reset and CoqIde, sidi
    - Re: [Coq-Club] Reset and CoqIde, Pierre Boutillier