aboutsummaryrefslogtreecommitdiff
path: root/vernac/g_proofs.mlg
AgeCommit message (Expand)Author
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
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