| Age | Commit message (Expand) | Author |
| 2007-07-13 | New bootstrapping, improved, Makefile system | corbinea |
| 2007-07-12 | normalisation (by closure) was not performed under fixpoints | barras |
| 2007-07-10 | Big reorganization of romega/ReflOmegaCore.v: towards a modular | letouzey |
| 2007-06-26 | Oups: thanks to ./configure -reals no, I was not building the whole dependenc... | letouzey |
| 2007-06-26 | additional properties for FMap (and slight rework of SetoidList and FSetPrope... | letouzey |
| 2007-06-21 | Simplification de la construction du .depend: | notin |
| 2007-06-21 | Adding: Field instance for Q. | roconnor |
| 2007-06-07 | Extension of NArith: Nminus, Nmin, etc | letouzey |
| 2007-03-22 | A tentative fix for bug #1455 | lmamane |
| 2007-03-06 | màj dépendances .v: SubtacTactics.vo | lmamane |
| 2007-02-19 | Correct coq depend, add eq_rect elimination tactic to SubtacTactics | msozeau |
| 2007-02-07 | Fix mistake naming my Tactics file Tactics :) | msozeau |
| 2007-02-05 | complement du commit 9591 | bgregoir |
| 2007-01-23 | Updated Makefile to include ConstructiveEpsilon.v | emakarov |
| 2007-01-10 | Merge from Lionel Elie Mamane's private branch: | lmamane |
| 2006-12-28 | Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à | herbelin |
| 2006-12-23 | Addition of a "Combined Scheme" vernacular command for building the conjuncti... | msozeau |
| 2006-12-15 | Changement dans ring et field, beaucoup de correction d'erreurs, | bgregoir |
| 2006-12-11 | Changement dans le kernel : | bgregoir |
| 2006-10-29 | Exports manquants dans ring | barras |
| 2006-10-27 | simplif de la partie ML de ring/field | barras |
| 2006-10-27 | changement des _sym par _comm dans setoid_ring | bgregoir |
| 2006-10-27 | Ajout ListTactics | herbelin |
| 2006-10-25 | oups, ne chargeait pas les bons fichiers | letouzey |
| 2006-10-25 | conflit de nom (Field_theory) modulo la casse | barras |
| 2006-10-05 | Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom | barras |
| 2006-09-28 | separation de RealField | barras |
| 2006-09-26 | petits pbs de dependances | barras |
| 2006-09-26 | Compilation newring | notin |
| 2006-09-26 | commit de field + renommages | barras |
| 2006-09-26 | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras |
| 2006-06-25 | nouvel algorithme pour Zgcd (plus rapide) + un Qcompare | letouzey |
| 2006-06-09 | Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT... | herbelin |
| 2006-06-05 | Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome d'ext... | letouzey |
| 2006-06-04 | Ajout exists! et restructuration/extension des fichiers sur la | herbelin |
| 2006-05-31 | ajout de QArith dans les theories standards | letouzey |
| 2006-05-22 | un debut de propriétés concernant FMap | letouzey |
| 2006-05-18 | Dépendances pour List.v | notin |
| 2006-05-16 | etoffage des notions de permutations (a la fois List.Permutation et Permutati... | letouzey |
| 2006-05-15 | ajout de theories/FSets/DecidableTypeEx.v | letouzey |
| 2006-05-15 | ajout d'exemples de decidable types | letouzey |
| 2006-05-11 | Duplication du fichier FSetProperties pour les ensembles Weak. | letouzey |
| 2006-05-03 | Cleanning and factorizing code in funind. Spliting new_arg_principles into to... | jforest |
| 2006-04-29 | suite de l'ajout des FSets/FMaps dans les theories standards | letouzey |
| 2006-04-26 | Régénération après mise à jour coqdep pour traiter Require multiple | herbelin |
| 2006-04-25 | Un gros coup de lifting pour IntMap: | letouzey |
| 2006-04-06 | versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes | letouzey |
| 2006-03-28 | reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere... | letouzey |
| 2006-03-17 | ajout d'un debut de proprietes pour les FSetWeak | letouzey |
| 2006-03-15 | Ajout de theories/FSets contenant la partie "light" de FSets et FMap: | letouzey |