Skip to Content.

Sympa Menu

coq-club - [Coq-Club] Subgoals for evars?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Subgoals for evars?

chronological Thread

From: Robin Green <greenrd AT greenrd.org>
To: coq-club AT inria.fr
Cc: Arnaud.Spiwack AT lix.polytechnique.fr
Subject: [Coq-Club] Subgoals for evars?
Date: Sun, 14 Mar 2010 12:14:45 +0000
Organization: Swansea University

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

Archive powered by MhonArc 2.6.16.