coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Subgoals for evars?

From: Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>
To: Robin Green <greenrd AT greenrd.org>
Cc: coq-club AT inria.fr
Subject: [Coq-Club] Re: Subgoals for evars?
Date: Sun, 14 Mar 2010 22:53:05 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=ksl++izff5ZwmPQcvBFPNUe9U9q0UnKvj1FCWLPvTuz3AHeLs/1rbKOciVEA5oIjVc pwthusPdubyzJpET0zTu718mqsPzp+a9Y7bpbK6buA8VVb4wpXQ76PiqzcsAFMmnkUC4 Q7zpNh1j7XxnONY0b6ZEAPeTY0p+vuQXHjpe8=

This won't be part of Coq v8.3, however next version of Coq will have this new proof engine. It should be noted, that it might very well be that by the next version the proof user interface (and tactic semantics) won't have changed at all. I'd hope not, but what I am about to commit to the trunk is something that enables to see all evars as goals and for compatibility reason, the old tactics have been ported without change of semantics onto it. Having a consistant set of tactics using the full power of the new proof engine is more work and not yet done (I have a very bad prototype in a corner of a sheet, though).

Arnaud Spiwack

On 14 March 2010 13:14, Robin Green <greenrd AT greenrd.org> wrote:

In 2007 Arnaud Spiwack mentioned in passing[1] an idea to rewrite Coq's
proof engine so that metavariables (a.k.a. evars) would become goals.

Has this idea been implemented?
--
Robin

[1] http://logical.saclay.inria.fr/coq-puma/messages/7f3e4de76e6200e5#msg-a36d7cb972fdd6d6

[Coq-Club] Subgoals for evars?, Robin Green
- [Coq-Club] Re: Subgoals for evars?, Arnaud Spiwack