coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Display of terms of record type in goal

From: Tom Prince <tom.prince AT ualberta.net>
To: "gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>, "Michael A. Warren" <mwarren AT ias.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Display of terms of record type in goal
Date: Thu, 27 Oct 2011 10:20:08 -0600

On Thu, 27 Oct 2011 15:08:31 +0100, "gallais @ ensl.org"
<guillaume.allais AT ens-lyon.org>
wrote:
> Hi Michael,
>
> You should be able to find what you are looking for here:
>
> http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/6524

The patches included in that thread have been applied to trunk and will
be in 8.4.

Tom

Re: [Coq-Club] Display of terms of record type in goal, Tom Prince