| Age | Commit message (Expand) | Author |
| 2007-01-22 | Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouent | herbelin |
| 2007-01-19 | Protection contre les warnings 'unused variable' de ocaml 3.09 | herbelin |
| 2007-01-15 | Various subtac fixes. | msozeau |
| 2007-01-12 | Suite au mail de Lionel a propos du Makefile: | letouzey |
| 2007-01-12 | un saut de ligne ... | letouzey |
| 2007-01-10 | Merge from Lionel Elie Mamane's private branch: | lmamane |
| 2007-01-10 | Nouvelle approche pour le discharge modulaire | herbelin |
| 2007-01-08 | Subtac fixes, support for reasoning on wf defs. | msozeau |
| 2007-01-05 | suite de la reparation du bug 1239: apres les inds, les records et vars de types | letouzey |
| 2007-01-02 | Rework subtac pattern matching equalities generation. | msozeau |
| 2006-12-28 | Remplacement de la définition de Pind et Prec par une définition | herbelin |
| 2006-12-22 | Default tactic for solving goals. | msozeau |
| 2006-12-21 | typo malencontreuse | filliatr |
| 2006-12-17 | reparation bug 1239 | letouzey |
| 2006-12-15 | Changement dans ring et field, beaucoup de correction d'erreurs, | bgregoir |
| 2006-12-15 | contrib/dp: tactique ergo (voir ergo.lri.fr) | filliatr |
| 2006-12-14 | Reimplemented equality generation for pattern matching at typing time. First ... | msozeau |
| 2006-12-12 | Subtac: work on cases. | msozeau |
| 2006-12-11 | Changement dans le kernel : | bgregoir |
| 2006-12-08 | contrib/dp | filliatr |
| 2006-12-08 | Subtac bug fix, add list take example. | msozeau |
| 2006-11-29 | Fork of cases impl for subtac. | msozeau |
| 2006-11-24 | Functional graph merging deals with letins. | courtieu |
| 2006-11-24 | Fixed the graph merging parameter order. | courtieu |
| 2006-11-23 | Fixing syntax and parameter order in functional graph merging. | courtieu |
| 2006-11-21 | Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de | herbelin |
| 2006-11-20 | Changing merging functional scheme syntax. | courtieu |
| 2006-11-20 | Suppression du type 'tac dans les abstract_argument_type: devenu inutile | herbelin |
| 2006-11-19 | mult_sym, plus_sym -> mult_comm, plus_comm | herbelin |
| 2006-11-16 | Small fix in functional graph merging. | courtieu |
| 2006-11-16 | suppression de code mort (avec bug de nom) | letouzey |
| 2006-11-16 | pb avec r9379 + modifs dans ring | barras |
| 2006-11-16 | Work on dep types pattern matching | msozeau |
| 2006-11-16 | suite de r9362: reconnaissance de qqs injections entre nat, N et Z | barras |
| 2006-11-15 | Some usability enhancements. | msozeau |
| 2006-11-13 | Better solve using tactics impl. | msozeau |
| 2006-11-13 | Correction de la seconde partie du bug #1278 | jforest |
| 2006-11-13 | Correction de la premiere partie du #1278 (but non referme en cas d'echec) | jforest |
| 2006-11-13 | Encore des _sym au lieu de _comm | herbelin |
| 2006-11-10 | generalisation de ring pour faire Ring_nf | barras |
| 2006-11-10 | Work on mutual defs, various bug fixes. | msozeau |
| 2006-11-10 | Work on pattern inequalities for pattern matching branches. | msozeau |
| 2006-11-09 | Support for mutual defs in obligation handling. | msozeau |
| 2006-10-31 | Debug obligation handling code | msozeau |
| 2006-10-31 | Fix compile error | msozeau |
| 2006-10-31 | Work on obligation separation. | msozeau |
| 2006-10-30 | fixed field_simplify + changed precedence of let and fun in ltac | barras |
| 2006-10-29 | Suite commit polymorphisme | herbelin |
| 2006-10-29 | Exports manquants dans ring | barras |
| 2006-10-28 | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin |