| Age | Commit message (Expand) | Author |
| 2007-07-25 | Modifications de la construction de la documentation de la librairie | notin |
| 2007-07-19 | Documentation of Program and its tactics, fix enormous interaction bug due to... | msozeau |
| 2007-07-13 | New bootstrapping, improved, Makefile system | corbinea |
| 2007-07-12 | port de r9968: bug avec les ring calculatoires | barras |
| 2007-07-09 | More natural notation for intro pattern: @a -> ?a | glondu |
| 2007-07-07 | If a fixpoint is not written with an explicit { struct ... }, then | letouzey |
| 2007-07-06 | Adding a syntax for "n-ary" rewrite: | letouzey |
| 2007-07-06 | extension of the rename tactic: the following is now allowed: | letouzey |
| 2007-07-06 | New intro pattern "@A", which generates a fresh name based on A. | glondu |
| 2007-07-06 | Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C)) | letouzey |
| 2007-07-05 | documentation of f_equal and revert and case_eq (and s/lri.fr/pps.jussieu.fr/... | letouzey |
| 2007-06-19 | typo faq | herbelin |
| 2007-06-08 | Removed an extra \tacindex occurrence for the tactic discriminate. | emakarov |
| 2007-06-07 | Ajout doc clear sans argument | herbelin |
| 2007-05-17 | Fixed bug #1540 (typo on name .coqide-gtk2rc) | herbelin |
| 2007-05-16 | - MAJ entêtes des fichiers produits par coq_makefile | herbelin |
| 2007-05-11 | Made some places in the reference manual clearer. Corrected | emakarov |
| 2007-04-29 | Ajout possibilité d'options à trois mots. | herbelin |
| 2007-04-26 | Documentation de Existential et de Show Existential (fixes bug #1294) | notin |
| 2007-04-18 | Fixed some typos. | glondu |
| 2007-04-17 | Corrected a LaTeX typo. | emakarov |
| 2007-04-17 | Changed many refman/*.tex files. Put \label and \index commands that immediat... | emakarov |
| 2007-04-16 | Removed from headers.hva the code to make index point to the section | emakarov |
| 2007-04-12 | Cleaned doc/common/title.tex file. Increased the space under headers | emakarov |
| 2007-04-12 | Standardisation format biblio | herbelin |
| 2007-04-10 | Some changes to eliminate Hevea warnings. | emakarov |
| 2007-04-10 | Split refman/headers.tex into headers.sty and headers.hva. | emakarov |
| 2007-04-10 | Eliminated warning messages from Hevea. Most warning messages were | emakarov |
| 2007-04-05 | Mise en place d'un rafinement de compute. | jforest |
| 2007-04-04 | Corrected a typo in doc/refman/Setoid.tex. | emakarov |
| 2007-03-16 | Correction du bug #1441 | notin |
| 2007-03-13 | Correction bug #1439 (comportement de replace by) | notin |
| 2007-03-07 | Application suggestion #1430 de Yevgeniy pour TEXINPUTS | herbelin |
| 2007-02-22 | doc: typo/english: "is left associating" -> "is left-associative". | lmamane |
| 2007-02-22 | Documentation of tactical "t1 || t2": t2 is executed if t1 fails to | lmamane |
| 2007-02-18 | Compilation de la FAQ | notin |
| 2007-02-15 | Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors | herbelin |
| 2007-02-13 | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin |
| 2007-02-07 | Meilleur anglais (cf 9619) | herbelin |
| 2007-02-07 | Relecture/nettoyage chapitre Gallina; déplacement section Function | herbelin |
| 2007-02-07 | Suppression RefMan-cas.tex inutilisé | herbelin |
| 2007-02-07 | Field rewrites only with polynomial | thery |
| 2007-02-07 | doc de ring/field + option infinite -> completeness | barras |
| 2007-02-06 | doc for field | thery |
| 2007-02-05 | complement du commit 9591 | bgregoir |
| 2007-02-01 | Report 9545 de 8.1 vers trunk | herbelin |
| 2007-02-01 | Petite relecture partie ring | herbelin |
| 2007-01-31 | report de r9574: doc de field | barras |
| 2007-01-31 | Fix typo. | msozeau |
| 2007-01-31 | Fix order of wf and measure arguments, patch Program doc. | msozeau |