coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Adam Chlipala <adam AT chlipala.net>
To: Stéphane Glondu <steph AT glondu.net>
Cc: Gregory Malecha <gmalecha AT eecs.harvard.edu>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Ltac Determine if a variable is an existential
Date: Tue, 09 Nov 2010 08:51:43 -0500

Stéphane Glondu wrote:

I am not aware of such thing built-in in Coq, but it is very easy to do in OCaml as a plugin

Since this issue would also block me from switching to 8.3, I've opened a bug suggesting that this plugin be added to the main codebase:
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2433

[Coq-Club] Ltac Determine if a variable is an existential, Gregory Malecha
- Re: [Coq-Club] Ltac Determine if a variable is an existential, Stéphane Glondu
  - Re: [Coq-Club] Ltac Determine if a variable is an existential, Adam Chlipala