aboutsummaryrefslogtreecommitdiff
path: root/vernac/pvernac.ml
AgeCommit message (Expand)Author
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-07-07Remove dead code that used to be there for CamlpX compatibility.Pierre-Marie Pédrot
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias