coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Kenneth Roe <kendroe AT hotmail.com>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] Efficient way to find non-instantiated external variables
Date: Tue, 26 Jul 2011 02:08:59 -0700
Importance: Normal

I have a proof that is a few hundred lines, involves many (nested) Coq calls, and takes about 15 minutes to complete. At the end, I have the error "No more subgoals but non-instantiated existential variables:...". What is the fastest way to find the exact lines of source code that are generating these goals?

- Ken

[Coq-Club] Efficient way to find non-instantiated external variables, Kenneth Roe
- Re: [Coq-Club] Efficient way to find non-instantiated external variables, Thomas Braibant
- Re: [Coq-Club] Efficient way to find non-instantiated external variables, Adam Chlipala