aboutsummaryrefslogtreecommitdiff
path: root/vernac/g_proofs.mlg
AgeCommit message (Expand)Author
2018-09-23[api] Deprecate constructors of deprecated datatypes.Emilio Jesus Gallego Arias
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-06-29Port g_proofs to the homebrew GEXTEND parser.Pierre-Marie Pédrot