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: Fri, 27 Mar 2009 11:34:37 -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=hl4KM9T3hhZUKkTlBxXTPjCgwqTHIG+qd2nQRYHQkA1JEDI5Ft3YwqcK8ReelPv6Qi tJGDypRT127Hz/PHYiQj7dt56Xt79SDFLol70ekG/dvja4EwzxdSs05ILKLx9kRWHaNc ENNTzV0E1RTNUvQrbSL7U1pdPQKljlo69aAJE=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Fri, Mar 27, 2009 at 2:23 AM, Florian Haftmann
<florian.haftmann AT informatik.tu-muenchen.de>
wrote:
> thanks for the answer. �This doesn't work either.

Probably still missing some assumptions.

> are equivalent, or at least this is what I thought the documentation says.

Not exactly.

> It would be helpful to have an explicit hint what is going on here.

Set Ltac Debug.

This will show you the actual environment under which your "using ..."
clause is being run. It is *not* the same as the (full) environment
you get with "escape".

--
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