The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> And some that are implemented in Ltac:
>
>   * tauto and intuition:
>     https://github.com/coq/coq/blob/v8.9/theories/Init/Tauto.v

tauto/intuition also have an ocaml part 
https://github.com/coq/coq/blob/v8.9/plugins/ltac/tauto.ml

Gaëtan Gilbert

On 08/03/2019 04:32, Joomy Korkut wrote:
> Hi Ray,
>
> It seems to be a bit of both. Here are some that are implemented in OCaml:
>
>   * the tactic definitions:
>     https://github.com/coq/coq/blob/v8.9/plugins/ltac/g_auto.ml4 (look
>     for `TACTIC EXTEND auto` and whatnot)
>   * auto: https://github.com/coq/coq/blob/v8.9/tactics/auto.ml
>   * eauto: https://github.com/coq/coq/blob/v8.9/tactics/eauto.ml
>
> And some that are implemented in Ltac:
>
>   * tauto and intuition:
>     https://github.com/coq/coq/blob/v8.9/theories/Init/Tauto.v
>
>
> Best,
> Joomy.
>
> > On Mar 7, 2019, at 7:13 PM, Xuanrui Qi <xqi01 AT cs.tufts.edu 
> > <mailto:xqi01 AT cs.tufts.edu>> wrote:
> >
> > Hello Coq-Clubbers,
> >
> > I am wondering how Coq's automation tactics (auto, tauto, intuition
> > which is just tauto fail, etc.) are implemented. Are they implemented
> > in Ltac or in OCaml (or perhaps some in Ltac and some in OCaml)? Could
> > someone point me to their implementations, if possible?
> >
> > Thanks!
> >
> > Best,
> > Ray
> >
> > --
> > Xuanrui (Ray) Qi
> >
> > xqi01 AT cs.tufts.edu
> >  
> > <mailto:xqi01 AT cs.tufts.edu>
> > me AT xuanruiqi.com
> > https://www.xuanruiqi.com