aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/Helm.tex
AgeCommit message (Expand)Author
2014-09-08Removing the documentation of the XML plugin.Pierre-Marie Pédrot
2012-08-11Improving rendering of ldots in doc (partially done, there are tooherbelin
2009-10-24Fixing XML doc (COQ_XML not working as an environment variable).herbelin
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2007-04-17Changed many refman/*.tex files. Put \label and \index commands that immediat...emakarov
2006-04-04Bug index addendum à cause mauvaise utilisation asection dans Helm.texherbelin
2006-02-23Nettoyage de l'archive doc et restructuration avant intégration à l'archiveherbelin