The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Jul 05, 2013 at 12:01:42AM -0700, t x wrote:
> Thanks for everyone's patient help. I think the problem here is that I'm
> confused about how ltac / goal states are working and thus unable to
> properly formulate a clear question.

I'm subscribed to this list, no need to CC

> 1) In Coq, just like how I can "Print" the definition of a function, can I
> also "Print" the definitions of tactics? (like: rewrite, refine, replace,
> exact) and see how they're implemented.
> 2) Is "refine" a Coq primitive (i.e. written in ocaml), or is it written in
> ltac? [and if so, where can I read the source]

All the tactics you mentioned are written in OCaml, look at the files in
the tactics/ directory.

Cheers
-- 
Enrico Tassi