| Age | Commit message (Expand) | Author |
| 2006-03-05 | New files for subtac | coq |
| 2006-03-05 | Renommage du IP classique pour éviter confusion avec IP constructif | herbelin |
| 2006-03-05 | Ajout étude IP généralisé, Gödel-Dummett, buveur | herbelin |
| 2006-03-05 | Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf... | herbelin |
| 2006-03-05 | Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf... | herbelin |
| 2006-03-05 | Ajout test relatif au bug #984 | herbelin |
| 2006-03-04 | Correction message d'erreur ltac et adoption du modèle de message de Tacinterp | herbelin |
| 2006-03-04 | maj | coq |
| 2006-03-04 | Petite simplification en passant | herbelin |
| 2006-03-04 | Titres moins envahissants pour coqdoc | herbelin |
| 2006-03-03 | maj | coq |
| 2006-03-02 | maj | coq |
| 2006-03-02 | Correction bug #1097 (dû à une typo...) | herbelin |
| 2006-03-02 | Ajout test bug 1089 | herbelin |
| 2006-03-02 | Correctif pour bug #1089 (cannot define an isevar twice) | herbelin |
| 2006-03-02 | tactic haRVey pour appeler haRVey (contrib/dp) | filliatr |
| 2006-03-02 | Correction du bug 808: il est maintenant interdit de déclarer une assomption... | coq |
| 2006-03-01 | Correction bug #842 (rename d'une hyp du contexte) | herbelin |
| 2006-03-01 | appel de Zenon | filliatr |
| 2006-02-28 | maj | coq |
| 2006-02-28 | *** empty log message *** | filliatr |
| 2006-02-27 | maj | coq |
| 2006-02-27 | quelques raccourcis commodes + un f_equal plus efficace | letouzey |
| 2006-02-27 | dp: sortie Why | filliatr |
| 2006-02-26 | maj | coq |
| 2006-02-25 | maj | coq |
| 2006-02-25 | changement de path du site web | narboux |
| 2006-02-25 | ajoute un warning sur htmlpp | narboux |
| 2006-02-24 | maj | coq |
| 2006-02-23 | maj | coq |
| 2006-02-23 | trying to fix a bug in pazrameter order in the multiple induction | coq |
| 2006-02-23 | Ajout 'exists! x:A, P (suite) | herbelin |
| 2006-02-23 | Ajout 'exists! x:A, P | herbelin |
| 2006-02-22 | maj | coq |
| 2006-02-22 | Minimum pour documentation TeX de la biblio | herbelin |
| 2006-02-22 | Work on recursive definitions | coq |
| 2006-02-22 | Add vernacular file for subtac | coq |
| 2006-02-22 | MAJ | herbelin |
| 2006-02-22 | Julien: | bertot |
| 2006-02-21 | maj | coq |
| 2006-02-21 | Work with binder lists, problem of tycons | coq |
| 2006-02-21 | Latest fixes, should work fine now for non recursive definitions, although st... | coq |
| 2006-02-20 | maj | coq |
| 2006-02-20 | Fix minor bug | coq |
| 2006-02-20 | Forgot a file | coq |
| 2006-02-20 | Monday work, working with coercions and implicit args | coq |
| 2006-02-20 | Forgot another file... | coq |
| 2006-02-20 | Forgot one file | coq |
| 2006-02-20 | Change in subtac modules | coq |
| 2006-02-20 | Rewrite of the subtac tactic, needs some work on implicit arguments. | coq |