coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Efficient way to find non-instantiated external variables

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Hendrik Tews <tews AT os.inf.tu-dresden.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Efficient way to find non-instantiated external variables
Date: Tue, 1 Nov 2011 09:47:13 -0400

I guess it would be a nice feature of Coq to produce a warning when
there are some existential variables left that don't appear in any
subgoals (and therefor won't be instantiated by "normal" tactics). It
would allow to find faster that a "eblah; eauto" was not a good idea!

My 2c.

Alexandre

Re: [Coq-Club] Efficient way to find non-instantiated external variables, Hendrik Tews
- Re: [Coq-Club] Efficient way to find non-instantiated external variables, Alexandre Pilkiewicz