aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/v8-syntax/syntax-v8.tex
Commit message (Expand)AuthorAge
* [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
* Remove Explain* vernacsGravatar glondu2010-10-06
* 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