coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Writing tactics with dependent destruction

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: Matthieu Sozeau <mattam AT mattam.org>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Writing tactics with dependent destruction
Date: Sun, 20 Jun 2010 02:50:43 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=FQIkbgfEnsRNVR47oDbyivPLx7vgg1xufjDK1Iseh7nEesMsMLNnTlmDKUgF0Yf+/B kGvLPhL/RBd4kUFgICC6Rq7HbSjAaOtn7hlsKnH4LIsZKuM08fM2GP+f5RxUwkb7JbXr xismp7Lwgu0WAhY0NmAoO5+17itr5AyDfRhlw=

>> If you redefine the notation like this it works:
>>
>> Tactic Notation "dependent" "destruction" hyp(H) :=
>> do_depelim' ltac:(fun hyp => do_case hyp) H.
>
> Is "do_depelim'" included in the Coq 8.3?
> (In Coq 8.2pl1, it doesn't seem to be.)

Interestingly, when I just rename the existing "do_depind'" to
"do_depelim'", it works.

[Coq-Club] Writing tactics with dependent destruction, Gyesik Lee
- Re: [Coq-Club] Writing tactics with dependent destruction, Matthieu Sozeau
  - Re: [Coq-Club] Writing tactics with dependent destruction, Gyesik Lee
    - Re: [Coq-Club] Writing tactics with dependent destruction, Gyesik Lee