-
Lukasz Czajka
- Logic-related components: translation, proof reconstruction,
automated reasoning tactics. Author of almost all OCaml/Ltac/Coq
code. Author of the
sauto
tactic.
- Logic-related components: translation, proof reconstruction,
automated reasoning tactics. Author of almost all OCaml/Ltac/Coq
code. Author of the
-
Cezary Kaliszyk
- Machine-learning component: premise selection. Author of the
predict
program.
- Machine-learning component: premise selection. Author of the
-
Burak Ekici
-
Preliminary version of boolean reflection in
sauto
. -
CVC4 integration.
-
-
Evan Marzion
- First version of hashing of lifted-out terms in the translation.
-
Thibault Gauthier
- Preliminary version of Coq data export.
-
Ping Hou
- Testing of the
sauto
tactic.
- Testing of the
-
Karl Palmskog
- Opam packaging, Travis CI configuration and Dune build scripts.
-
Other contributors listed on GitHub
- Small bugfixes and keeping up-to-date with Coq master.