aboutsummaryrefslogtreecommitdiff
path: root/vernac/comCoercion.mli
AgeCommit message (Expand)Author
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot