Skip to content

A generic goal preprocessing tool for proof automation tactics in Coq

License

Notifications You must be signed in to change notification settings

QuentinCanu/trakt

 
 

Repository files navigation

Trakt logo

Trakt

This repository contains the first version of Trakt, a generic goal preprocessing tool for proof automation tactics in Coq.

NB: for users having a version of Coq older than 8.15, there is a branch with support for Coq 8.13.

About

A generic goal preprocessing tool for proof automation tactics in Coq

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Prolog 79.2%
  • Coq 20.6%
  • Makefile 0.2%