aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/v8-syntax
Commit message (Expand)AuthorAge
* Add dev/v8-syntax/check-grammar byproducts to gitignore.Gravatar Gaëtan Gilbert2017-08-01
* Fix syntax-v8.tex bad parenthesizingGravatar Gaëtan Gilbert2017-08-01
* [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
* Remove Explain* vernacsGravatar glondu2010-10-06
* Remove bashismsGravatar glondu2010-01-28
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* first-order --> firstorder (kills a warning about not being a valid id)Gravatar letouzey2008-04-16
* Restructuration dossier dev et mise à jour de certaines documentationsGravatar herbelin2006-05-23