aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/g_proofs.mlg
Commit message (Expand)AuthorAge
* Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-07-07
* hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
* Port g_proofs to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29