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