aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.coq
Commit message (Expand)AuthorAge
* Oups: thanks to ./configure -reals no, I was not building the whole dependenc...Gravatar letouzey2007-06-26
* additional properties for FMap (and slight rework of SetoidList and FSetPrope...Gravatar letouzey2007-06-26
* Simplification de la construction du .depend:Gravatar notin2007-06-21
* Adding: Field instance for Q.Gravatar roconnor2007-06-21
* Extension of NArith: Nminus, Nmin, etcGravatar letouzey2007-06-07
* A tentative fix for bug #1455Gravatar lmamane2007-03-22
* màj dépendances .v: SubtacTactics.voGravatar lmamane2007-03-06
* Correct coq depend, add eq_rect elimination tactic to SubtacTacticsGravatar msozeau2007-02-19
* Fix mistake naming my Tactics file Tactics :)Gravatar msozeau2007-02-07
* complement du commit 9591Gravatar bgregoir2007-02-05
* Updated Makefile to include ConstructiveEpsilon.vGravatar emakarov2007-01-23
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àGravatar herbelin2006-12-28
* Addition of a "Combined Scheme" vernacular command for building the conjuncti...Gravatar msozeau2006-12-23
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Exports manquants dans ringGravatar barras2006-10-29
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
* Ajout ListTacticsGravatar herbelin2006-10-27
* oups, ne chargeait pas les bons fichiersGravatar letouzey2006-10-25
* conflit de nom (Field_theory) modulo la casseGravatar barras2006-10-25
* Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynomGravatar barras2006-10-05
* separation de RealFieldGravatar barras2006-09-28
* petits pbs de dependancesGravatar barras2006-09-26
* Compilation newringGravatar notin2006-09-26
* commit de field + renommagesGravatar barras2006-09-26
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* nouvel algorithme pour Zgcd (plus rapide) + un QcompareGravatar letouzey2006-06-25
* Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...Gravatar herbelin2006-06-09
* Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome d'ext...Gravatar letouzey2006-06-05
* Ajout exists! et restructuration/extension des fichiers sur laGravatar herbelin2006-06-04
* ajout de QArith dans les theories standardsGravatar letouzey2006-05-31
* un debut de propriétés concernant FMapGravatar letouzey2006-05-22
* Dépendances pour List.vGravatar notin2006-05-18
* etoffage des notions de permutations (a la fois List.Permutation et Permutati...Gravatar letouzey2006-05-16
* ajout de theories/FSets/DecidableTypeEx.vGravatar letouzey2006-05-15
* ajout d'exemples de decidable typesGravatar letouzey2006-05-15
* Duplication du fichier FSetProperties pour les ensembles Weak. Gravatar letouzey2006-05-11
* Cleanning and factorizing code in funind. Spliting new_arg_principles into to...Gravatar jforest2006-05-03
* suite de l'ajout des FSets/FMaps dans les theories standardsGravatar letouzey2006-04-29
* Régénération après mise à jour coqdep pour traiter Require multipleGravatar herbelin2006-04-26
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
* reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere...Gravatar letouzey2006-03-28
* ajout d'un debut de proprietes pour les FSetWeakGravatar letouzey2006-03-17
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
* Modularisation des preuves concernant la logique classique, l'indiscernabilit...Gravatar herbelin2006-03-05
* majGravatar coq2006-02-22
* Zmax et ZminmaxGravatar herbelin2006-02-12