coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Cezar proof text transformation

From: Taral <taralx AT gmail.com>
To: Florian Haftmann <florian.haftmann AT informatik.tu-muenchen.de>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Cezar proof text transformation
Date: Thu, 26 Mar 2009 09:53:22 -0700
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:content-transfer-encoding; b=rDuHouH+P+y1X6chp4k0SmiNPIfhMY+eqDGW3SO6TizmertQzcPiwq2HjO3nOswvoY P2+6csTTA8YFVWEIWjYj9yeQU7pnaqW1DnTV5nWgV8qf57CJz5Zwpo4+qbNiqZ1f35qz GX1QR06LmA84BIjsAt8Lzi8VMUpuQ5YE5eC4I=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Mar 25, 2009 at 2:11 AM, Florian Haftmann
<florian.haftmann AT informatik.tu-muenchen.de>
wrote:
> � � �thus (S q + s = n)
> � � � �using rewrite n_Sr; simpl; rewrite qsr; reflexivity.

You probably need to have "by n_Sr, qsr". The using-clause only has
the minimum number of assumptions available to it.

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

[Coq-Club] Cezar proof text transformation, Florian Haftmann
- Re: [Coq-Club] Cezar proof text transformation, Taral
  - Re: [Coq-Club] Cezar proof text transformation, Florian Haftmann
    - Re: [Coq-Club] Cezar proof text transformation, Taral
      - Re: [Coq-Club] Cezar proof text transformation, Florian Haftmann