aboutsummaryrefslogtreecommitdiff
path: root/vernac/printmod.ml
AgeCommit message (Expand)Author
2021-01-13Make sure "Print Module" write a dot at the end of inductive definitions.Guillaume Melquiond
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-06-30[declaremods] Remove abstraction of imperative module operationsEmilio Jesus Gallego Arias
2020-06-30[states] Move States to vernacEmilio Jesus Gallego Arias