coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
- To: AUGER Cédric <sedrikov AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Coq improvement in 8.4
- Date: Sat, 29 Sep 2012 00:08:38 +0800
Funny. A more natural version would be:
And, more minimalist (without assuming True):
refine (λ H, match H with eq_refl => H end).
It already works with 8.3.pl4, but not 8.2pl1
(even the exact term does not type check).
On Fri, Sep 28, 2012 at 05:11:26PM +0200, AUGER Cédric wrote:
> I wanted to manually perform a "discriminate", and I did something
> like:
>
> Lemma Z : true = false → False.
> refine (λ H, match H with eq_refl => True end).
> Defined.
>
> I am pretty sure it used not to work (I am on a 8.4 trunk version) on
> 8.3. So I was very surprised to see it working, and I feared a bug.
>
> Print Z.
>
> Hopefully returns something that I recognize to be correct. So now
> pattern matching on Coq seems more clever than in 8.3. So I was
> wondering from when such an improvement occured and if there was some
> other nice improvement in the same spirit (I did not find it in the
> Changelog…).
- [Coq-Club] Coq improvement in 8.4, AUGER Cédric, 09/28/2012
- Re: [Coq-Club] Coq improvement in 8.4, Jean-Francois Monin, 09/28/2012
- Re: [Coq-Club] Coq improvement in 8.4, Daniel Schepler, 09/28/2012
Archive powered by MHonArc 2.6.18.