Skip to Content.

Sympa Menu

coq-club - [Coq-Club] discriminate tactic and identity types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] discriminate tactic and identity types

chronological Thread

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq-Club Club <coq-club AT inria.fr>
Cc: Vladimir Aleksandrovich Voevodsky <vladimir AT ias.edu>
Subject: [Coq-Club] discriminate tactic and identity types
Date: Tue, 24 May 2011 14:10:06 -0400

I wonder if there is an easy way to make discriminate work with [ identity ]
instead of [ eq ] ?

Vladimir.

[Coq-Club] discriminate tactic and identity types, Vladimir Voevodsky
- Re: [Coq-Club] discriminate tactic and identity types, Hugo Herbelin

Archive powered by MhonArc 2.6.16.