aboutsummaryrefslogtreecommitdiff
path: root/dev/v8-syntax
AgeCommit message (Expand)Author
2018-09-25Remove romegaVincent Laporte
2017-08-01Add dev/v8-syntax/check-grammar byproducts to gitignore.Gaëtan Gilbert
2017-08-01Fix syntax-v8.tex bad parenthesizingGaëtan Gilbert
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2015-12-07Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2010-12-24Remove obsolete script univdot, update dev doc about universesglondu
2010-10-06Remove Explain* vernacsglondu
2010-01-28Remove bashismsglondu
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2008-04-16first-order --> firstorder (kills a warning about not being a valid id)letouzey
2006-05-23Restructuration dossier dev et mise à jour de certaines documentationsherbelin