coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Setoid rewrite and currying

From: Taral <taralx AT gmail.com>
To: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
Cc: 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 13:11:50 -0700
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:content-transfer-encoding; b=mkFzFZZbABqL9jF/qL81ZXt3rCSozJgDHDWAuxBhaxkPs5bLOvbLw3VI8G2N4bQhuZ uH6HdMinRZ5XLKdNZQNQWPSgJRedkzsIbbit5TzD9AIlpU7DXPvVr1PyxJ7yEAgH6Nyi eDx0INKyHKDfru2dWokfU0nKTfv8FH7OYi7pc=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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?

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

[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