Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq improvement in 8.4

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq improvement in 8.4


Chronological Thread 
  • 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…).



Archive powered by MHonArc 2.6.18.

Top of Page