coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Setoid rewrite and currying

From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
To: Arnaud Spiwack <arnaud.spiwack AT gmail.com>
Cc: Taral <taralx AT gmail.com>, Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Setoid rewrite and currying
Date: Fri, 24 Apr 2009 22:31:20 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=CMlO9wArq/fRI/7Z/9BPXGniJOs78pKv6UbsoxH0HLs0cbdusTHQiWPIM7fej9IQ1F jP+pkMSc0GK+1QjAQwHBhSN/4elkpzMLCQ5QN2je+ZzG/DGxBjIKR720EA6i24UPc/nM D4eShDfyjPqoq5x9j24uoCl0mcWXXut1wHZ94=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thanks Matthieu, it worked fine here now. Great job by the way!

On Fri, Apr 24, 2009 at 9:15 PM, Arnaud Spiwack <arnaud.spiwack AT gmail.com> wrote:

Ssreflect.

But equivalently (mostly) you could write "intros [ ? ? [ ? ? ? ]]; auto".

Arnaud Spiwack

Taral a écrit :

On Fri, Apr 24, 2009 at 2:26 AM, Arthur Azevedo de Amorim
<arthur.aa AT gmail.com> wrote:

Proof. move => [? ? [? ? ?]]; auto. Qed.

This line fails for me. What am I missing?

--
Arthur Azevedo de Amorim

[Coq-Club] Setoid rewrite and currying, Arthur Azevedo de Amorim
- Re: [Coq-Club] Setoid rewrite and currying, Arnaud Spiwack
  - Re: [Coq-Club] Setoid rewrite and currying, Arthur Azevedo de Amorim
    - Re: [Coq-Club] Setoid rewrite and currying, Matthieu Sozeau
    - Re: [Coq-Club] Setoid rewrite and currying, Taral
      - Re: [Coq-Club] Setoid rewrite and currying, Arnaud Spiwack
        
        Re: [Coq-Club] Setoid rewrite and currying, Arthur Azevedo de Amorim