coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Reset Induction Principle

From: Georges Gonthier <gonthier AT microsoft.com>
To: Qiang Liu <lqiangecnu AT gmail.com>, "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: RE: [Coq-Club] Reset Induction Principle
Date: Wed, 9 Dec 2009 12:18:50 +0000
Accept-language: en-GB, en-US
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Try using Unset Elimination Schemes (8.14.1 in the manual) instead.

Cheers.

From: coq-club-admin AT pauillac.inria.fr [mailto:coq-club-admin AT pauillac.inria.fr] On Behalf Of Qiang Liu
Sent: 09 December 2009 01:39
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Reset Induction Principle

Hello, everyone:

i defined a inductive type, like : Inductive Term : Set. However, i do not want to use the induction principle Term_ind, because it is too weak. So how can i reset it in the CoqIDE ?

ps: I tried the command Reset, it says: Use CoqIDE navigation instead!

Thanks

[Coq-Club] Reset Induction Principle, Qiang Liu
- RE: [Coq-Club] Reset Induction Principle, Georges Gonthier