Implementation of tactics at the OCaml level

[David Pereira-3]

Hi all,

Does anyone know of some simple examples about how to implement coq  
tactics (version 8.2) directly in OCaml?

Best regards,
    David.

David Pereira
MAP-i Phd Student in Computer Science
Researcher at LIACC - UP
Contacts : dpereira_at_liacc_dot_up_dot_pt
                    ([phone]

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club