coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Setoid rewrite and currying

From: Arnaud Spiwack <arnaud.spiwack AT gmail.com>
To: Taral <taralx AT gmail.com>
Cc: Arthur Azevedo de Amorim <arthur.aa 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:15:06 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:cc:subject :references:in-reply-to:content-type:content-transfer-encoding; b=pI0xeLvTdfiCzYG9bGQ3jgV+tnolKO1u2oUwlwkBbEgpJZ11zTXhpGqv0kdKvJELUL wBZ7sC88PWtA5fkkNRSveWJW3Fonap58Ti7MwFQ64jd4rM31XYGv1Om4blA5rTDxUqn3 +Ykxu61cl7yLbtmtAoxovuvvmwRb9wrXoLHho=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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?

[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