coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vilhelm Sj�berg <vilhelm AT cis.upenn.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] change in behavior from 8.2pl3 to 8.3rc1 -- bug?
- Date: Mon, 20 Sep 2010 14:43:28 -0400
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:message-id:date:from:user-agent:mime-version:to:subject :references:in-reply-to:content-type:content-transfer-encoding; b=uEnxGmRqjDlB6d2c68uyKl5+QPEuKAy7B4ua/BFQpsRn5UEiymnBZR/hYbVyqGovDO VVh3ExRDc2n5n/UhUfcL1ZMli8AkMWiiAa4FIMM+zk4OLszj0P5Z50r/UQLUBovWu1JQ YEESHFRvSQ4K8bxm7zqF/xtSPGyU4ZmWga9Ww=
On 2010-20-09 14:28, Adam Megacz wrote:
(* The script below works with 8.2pl3 but reports "Error: Unbound and
* ungeneralizable variable A" with 8.3rc1 *
Adding
Generalizable All Variables.
to the top of the file seems to fix the problem. This is one of the new commands mentioned in
http://www.lix.polytechnique.fr/coq/distrib/V8.3-beta0/CHANGES
.
Vilhelm Sjöberg
- [Coq-Club] change in behavior from 8.2pl3 to 8.3rc1 -- bug?, Adam Megacz
- Re: [Coq-Club] change in behavior from 8.2pl3 to 8.3rc1 -- bug?, Vilhelm Sjöberg
- Re: [Coq-Club] change in behavior from 8.2pl3 to 8.3rc1 -- bug?, Matthieu Sozeau
Archive powered by MhonArc 2.6.16.