| Age | Commit message (Expand) | Author |
| 2007-10-07 | Détection de camlp5 5.00 au configure | herbelin |
| 2007-10-07 | Ajout de la possibilité de donner le chemin de la bibliothèque camlp5 | herbelin |
| 2007-10-06 | Allowing infix constructors/types in a Extract Inductive | letouzey |
| 2007-10-06 | Extraction: factorisation of identical branches in a match | letouzey |
| 2007-10-05 | Correction du bug #1715 | notin |
| 2007-10-05 | petite reparation de la config pour camlp5 apres le commit 10164 | letouzey |
| 2007-10-05 | Added the automatic generation of the boolean equality if possible and the | vsiles |
| 2007-10-05 | Correction de quelques défauts d'affichage (notations sous "as" pour | herbelin |
| 2007-10-04 | Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o... | emakarov |
| 2007-10-04 | Ajout option -lablgtkdir au configure (basé sur patch de Guillaume | herbelin |
| 2007-10-04 | Bug 1716: Scheme now print the right messages | vsiles |
| 2007-10-04 | Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars) | herbelin |
| 2007-10-03 | Compilation sous windows | notin |
| 2007-10-03 | Révision de theories/Logic concernant les axiomes de descriptions. | herbelin |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-10-03 | BigZ now are proved | thery |
| 2007-10-02 | The following now compiles: abstract integers with plus, minus and times, bin... | emakarov |
| 2007-10-02 | Preventing gcc to generate dependencies wrt OCaml files (otherwise, we run in... | notin |
| 2007-10-02 | Fix a problem doing 'make clean' under Winodws | notin |
| 2007-10-02 | Report des modifications faites sur le configure en r10039, r10052, r10053 et... | notin |
| 2007-10-02 | Now NMake is proved | thery |
| 2007-10-02 | Correcting error message when adding Setoid, Relation or morphism (bug #1626) | jforest |
| 2007-10-01 | Added the compilation of theories/Numbers to Makefile.common. The following t... | emakarov |
| 2007-10-01 | Nouvelle mise à jour | herbelin |
| 2007-10-01 | Amendement à la révision 10124 : déplacement de apprec_nohdbeta entre | herbelin |
| 2007-10-01 | Complément nécessaire aux révisions 10156 et 10157 | herbelin |
| 2007-09-30 | Suite de 10157 | herbelin |
| 2007-09-30 | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin |
| 2007-09-28 | Creation of a new token PATTERNIDENT (?ident) for intro patterns, so | glondu |
| 2007-09-28 | On empêche "fresh" d'engendrer un mot-clé. | herbelin |
| 2007-09-28 | On Linux, we read /proc/self/exe to get the executable's path instead | glondu |
| 2007-09-28 | Correction bug 1711 | herbelin |
| 2007-09-28 | Oubli dans Setoid.v | notin |
| 2007-09-28 | Forget to update the CHANGES file | vsiles |
| 2007-09-28 | Modification of the Scheme command. | vsiles |
| 2007-09-27 | Découpage de Setoid.v | notin |
| 2007-09-27 | Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0 | herbelin |
| 2007-09-26 | Complément aux commits 10124 et 10125 sur l'inférence de type (correction | herbelin |
| 2007-09-26 | added a lemma to prove inj_pair2 when eq_dec is available. | vsiles |
| 2007-09-25 | An update on theories/Numbers. | emakarov |
| 2007-09-25 | Changes in Backtrack documentation. More accurate. | courtieu |
| 2007-09-25 | Suppression de tous les alias de la forme x:=x dans la compilation du filtrage. | herbelin |
| 2007-09-24 | Added the documentation for Backtrack and BackTo. | courtieu |
| 2007-09-21 | curpat_ty was in a smaller context | msozeau |
| 2007-09-21 | Petit complément au commit 10131. | herbelin |
| 2007-09-21 | Correction d'un bug dans check + ajout de tests | notin |
| 2007-09-21 | Update on theories/Numbers | emakarov |
| 2007-09-21 | Update on theories/Numbers. Natural numbers are mostly complete, | emakarov |
| 2007-09-21 | - Fixing bug 1703 ("intros until n" falls back on the variable name when | herbelin |
| 2007-09-20 | Changed the definition of Nminus in BinNat.v by removing comparison. | emakarov |