aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacextend.mli
AgeCommit message (Expand)Author
2019-05-23Fixing typos - Part 3JPR
2019-05-20Remove VtUnknown classificationMaxime Dénès
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-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