coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Announcing Coq 8.3-beta0

From: Taral <taralx AT gmail.com>
To: Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Announcing Coq 8.3-beta0
Date: Wed, 17 Feb 2010 16:58:51 -0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=N8wC6F7cdk54c7kPKQFVTWD23N3V8nWxaKkgrbYF/8hRr5iS58aoUvNKHXPrM7E5bU 8J6llVTDpGUv2QLMKRmiGozQjcJz1Ehk662sERJ6UvvQYEtHju97Vk3/gHjl1rM8M9AE dRksyifhe/CQVkf5ZTqAM8+xGe3Zc9izMLmwE=

On Wed, Feb 17, 2010 at 7:24 AM, Pierre Letouzey
<Pierre.Letouzey AT pps.jussieu.fr>
wrote:
> We're glad to announce the availability of a first _beta_ version of
> Coq 8.3, whose source files can be found on the Coq website [1].
> This release intends to give the curious and impatient users of Coq
> a flavour of what Coq 8.3 will be, and to encourage early testing and
> feedback. To see what is new in this version of Coq, please refer to
> the CHANGES [2] file.

Yay, patterns in change!

Am I doing it wrong?

  X : Prop
  ============================
   X -> False -> False

Unnamed_thm < change (?t -> False) with (not t).
Anomaly: uncaught exception Not_found. Please report.

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown

[Coq-Club] Announcing Coq 8.3-beta0, Pierre Letouzey
- Re: [Coq-Club] Announcing Coq 8.3-beta0, Taral