aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Makefile
Commit message (Expand)AuthorAge
* ajout du document sur la nouvelle syntaxeGravatar barras2001-12-11
* dvips -o ==> dvips -o $@Gravatar coq2000-07-26
* docGravatar herbelin2000-06-02
* documentationGravatar filliatr1999-12-13
* un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
* doc minicoq (grammaires)Gravatar filliatr1999-09-07
* documentation (prog literaire)Gravatar filliatr1999-08-19