coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Programming custom Tactics, Christian Doczkal
- <Possible follow-ups>
- [Coq-Club] Programming custom Tactics,
Christian Doczkal
- Re: [Coq-Club] Programming custom Tactics,
Sean Wilson
- Re: [Coq-Club] Programming custom Tactics,
Christian Doczkal
- Re: [Coq-Club] Programming custom Tactics,
Pierre Corbineau
- Re: [Coq-Club] Programming custom Tactics,
Christian Doczkal
- Re: [Coq-Club] Programming custom Tactics, Pierre Corbineau
- Re: [Coq-Club] Programming custom Tactics, Matthieu Sozeau
- Re: [Coq-Club] Programming custom Tactics,
Christian Doczkal
- Re: [Coq-Club] Programming custom Tactics, Vladimir Komendantsky
- Re: [Coq-Club] Programming custom Tactics,
Pierre Corbineau
- Re: [Coq-Club] Programming custom Tactics,
Christian Doczkal
- Re: [Coq-Club] Programming custom Tactics,
Sean Wilson
Archive powered by MhonArc 2.6.16.