aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/CHANGES
AgeCommit message (Collapse)Author
2019-05-23Fixing typos - Part 2JPR
2017-10-19Moving bug numbers to BZ# format in the source code.Théo Zimmermann
Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
2015-10-13Fix some typos.Guillaume Melquiond
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7