aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Helm.tex
Commit message (Expand)AuthorAge
* Removing the documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Improving rendering of ldots in doc (partially done, there are tooGravatar herbelin2012-08-11
* Fixing XML doc (COQ_XML not working as an environment variable).Gravatar herbelin2009-10-24
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* Changed many refman/*.tex files. Put \label and \index commands that immediat...Gravatar emakarov2007-04-17
* Bug index addendum à cause mauvaise utilisation asection dans Helm.texGravatar herbelin2006-04-04
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23