| Age | Commit message (Expand) | Author |
| 2003-12-21 | Ajout symmetry in; NArithRing; Hint Local; MAJ V8; typos | herbelin |
| 2003-12-20 | Typo | herbelin |
| 2003-12-19 | Correction de la grammaire des intro-patterns | herbelin |
| 2003-12-19 | Documentation 'inversion as' | herbelin |
| 2003-12-19 | *** empty log message *** | barras |
| 2003-12-19 | *** empty log message *** | barras |
| 2003-12-19 | Petits changements dans la doc de functional scheme et functional induction. | coq |
| 2003-12-19 | COQBIN plus necessaire, typos | marche |
| 2003-12-19 | passe sur les labels et les refs dans chapitres tactiques | filliatr |
| 2003-12-18 | premiere passe V8 | filliatr |
| 2003-12-18 | encore un peu de tactiques... | filliatr |
| 2003-12-17 | encore un peu de tactiques... | filliatr |
| 2003-12-17 | MAJ induction/destruct/simpl | herbelin |
| 2003-12-16 | tactiques | filliatr |
| 2003-12-12 | typo | marche |
| 2003-12-02 | relecture JCF | filliatr |
| 2003-12-02 | added Firstordre and Congruence | corbinea |
| 2003-11-23 | Label redondant | herbelin |
| 2003-10-30 | Added a tactic entry for Jprover + commented out inputenc in the main file | corbinea |
| 2003-10-27 | MAJ Double Inductive vis a vis de la V7.4 | herbelin |
| 2003-09-25 | passage V8 | filliatr |
| 2003-06-21 | Added the documentation on Functional Scheme (a command, I also put | courtieu |
| 2003-05-20 | Ajout 'in (Type of ...)' | herbelin |
| 2003-03-21 | MAJ Simpl et Change | herbelin |
| 2002-09-16 | Correction typo d'un but Tauto | herbelin |
| 2002-09-16 | documentation variante Subst (sans argument) | filliatr |
| 2002-09-12 | Subst | filliatr |
| 2002-09-09 | MAJ syntaxe 'Hint Rewrite' | herbelin |
| 2002-05-16 | MAJ V7.3 | herbelin |
| 2002-04-12 | doc Intuition et Tauto | courant |
| 2002-04-11 | Ajout Rename et Pose | herbelin |
| 2002-03-01 | Quelques pr�cisions sur la convertibilit� et les tactiques Cbv/Lazy | herbelin |
| 2001-12-23 | Ajout ClearBody et Assert H:=t | herbelin |
| 2001-10-15 | Ajout fonctionnalit� Intros Until de Injection, Discriminate et Simplify_eq | herbelin |
| 2001-10-09 | Adding documentation for a variant of Inversion, where a numeric argument, | bertot |
| 2001-10-02 | MAJ Intro + divers | herbelin |
| 2001-09-21 | Diverses MAJ V7.1 autour des qualid | herbelin |
| 2001-09-14 | Documentation NewInduction, NewDestruct, LetTac, Assert | herbelin |
| 2001-04-24 | Fourier, Reals,... | mayero |
| 2001-04-23 | Ajout d'une ref pour Field | delahaye |
| 2001-04-23 | Ajout de Field | delahaye |
| 2001-04-19 | Changement de Zarith en ZArith | mohring |
| 2001-04-12 | Intros Pattern wildcard | mohring |
| 2001-04-10 | MAJ decompose | herbelin |
| 2001-04-08 | Revision Tauto, AutoRewrite + Ajout de Ltac | delahaye |
| 2001-04-06 | mise a jour V7 | filliatr |
| 2001-04-06 | mise a jour V7 | filliatr |
| 2000-12-12 | Initial revision | filliatr |