coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Programming custom Tactics

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, Vladimir Komendantsky