coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] case splitting on the presense of existential variables

From: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] case splitting on the presense of existential variables
Date: Thu, 15 May 2008 23:45:34 +0900 (JST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello.

Can I define a tactic which can examine whether the goal contains
existential variables?
I.e. I want to change the behavior of a tactic depending on whether or not
the goal contains existential variables.

With best,
Keiko

[Coq-Club] case splitting on the presense of existential variables, Keiko Nakata