Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] user-defined tactic in some hypothesis

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] user-defined tactic in some hypothesis


chronological Thread 
  • From: "Andrew McCreight" <continuation AT gmail.com>
  • To: frederic.blanqui AT loria.fr
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] user-defined tactic in some hypothesis
  • Date: Thu, 29 May 2008 06:04:07 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:references; b=xOVZq9vut9Tkn/n9ykGE04qjGHiyI6cV5VjT/YnYNptTlSLGAXJnqwR3ge/Z77sJsvtTjmxUyeKb7PnG5xIgBxmlArgrQNidKepG3M0UI7VEv82tvx53lI9sxHAvv5rWfaDlRn4dCOwzzq+ukvWPcbNHWzr/+hCIXG1SrhD6i1A=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
This might not be quite what you are looking for, but you can manually define a variant of your tactic with "in" using Tactic Notation.

For a number of examples, look here:

http://logical.futurs.inria.fr/cocorico/Folding%20tactics

-Andrew

On Wed, May 28, 2008 at 11:37 PM, <frederic.blanqui AT loria.fr> wrote:

hello. it is possible to apply some built-in tactics in some hypothesis using the "in" keyword. but it does not seem possible to do the same for user-defined (with ltac) tactics. is there a way to do that i do not know? otherwise, would it be difficult to add this in coq? thanks.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


Archive powered by MhonArc 2.6.16.

Top of Page