aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacextend.ml
AgeCommit message (Expand)Author
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-03-31Multiple payload types in tokensPierre Roux
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-23Remove the unsafe camlp5 API from the Coq codebase.Pierre-Marie Pédrot
2018-11-23change vernac_qed_type to have [VtKeep of vernac_keep_as]Gaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias