Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Programming custom Tactics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Programming custom Tactics


chronological Thread 
  • From: Vladimir Komendantsky <komendantsky AT gmail.com>
  • To: Christian Doczkal <doczkal AT ps.uni-sb.de>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Programming custom Tactics
  • Date: Mon, 11 Jan 2010 16:39:08 +0000
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=i3zFgIiLm/6pkKJQ09B9G+KoIOp7Ju98iukubPkCZIrN4eG/gcC176007mzdCWg49b AuymInOFCyktz0PXv4qTG6mVBWaacCeiUS0yaTIP782sLsKv1nwa3UFUByjCv3Fa8qrY X0FiM9ITmDAhF51+wUhFHPS7ml5A7hnfs18tY=

> So what else do I have to do, to actually be able to call the linked in
> tactic? I have renamed the function "absurd" in the .mi as well as in
> the .mli file.

You must extend grammar rules. This should probably look as follows:

(*i camlp4use: "pa_extend.cmo" i*)
(*i camlp4deps: "parsing/grammar.cma" i*)

TACTIC EXTEND absurd
 [ "absurd" constr(c) ] -> [ your_absurd_fun c ]
END

This is the way it is actually implemented in
tactics/extratactics.ml4. There are more examples in other ml4 files.
The files parsing/g_vernac.ml4 and parsing/g_tactic.ml4 may be
informative.

Best wishes,
Vladimir



Archive powered by MhonArc 2.6.16.

Top of Page