coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] CoqIde and subgoal IDs vs. evar IDs

From: Jonathan <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] CoqIde and subgoal IDs vs. evar IDs
Date: Tue, 02 Sep 2014 16:56:25 -0400

When working in ProofGeneral and using the new dependent subgoal feature, a subgoal for evar ?N is subgoal ID=N. That's very useful when working with several evar subgoals with the same type. However, unlike ProofGeneral, CoqIde doesn't display subgoal IDs by default. Is there a way to make it do so?

-- Jonathan

[Coq-Club] CoqIde and subgoal IDs vs. evar IDs, Jonathan, 09/02/2014