| Commit message (Expand) | Author | Age |
* | Fix mistake naming my Tactics file Tactics :) | msozeau | 2007-02-07 |
* | complement du commit 9591 | bgregoir | 2007-02-05 |
* | Updated Makefile to include ConstructiveEpsilon.v | emakarov | 2007-01-23 |
* | Merge from Lionel Elie Mamane's private branch: | lmamane | 2007-01-10 |
* | Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à | herbelin | 2006-12-28 |
* | Addition of a "Combined Scheme" vernacular command for building the conjuncti... | msozeau | 2006-12-23 |
* | Changement dans ring et field, beaucoup de correction d'erreurs, | bgregoir | 2006-12-15 |
* | Changement dans le kernel : | bgregoir | 2006-12-11 |
* | Exports manquants dans ring | barras | 2006-10-29 |
* | 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-27 |
* | oups, ne chargeait pas les bons fichiers | letouzey | 2006-10-25 |
* | conflit de nom (Field_theory) modulo la casse | barras | 2006-10-25 |
* | Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom | barras | 2006-10-05 |
* | separation de RealField | barras | 2006-09-28 |
* | 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-09-26 |
* | nouvel algorithme pour Zgcd (plus rapide) + un Qcompare | letouzey | 2006-06-25 |
* | Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT... | herbelin | 2006-06-09 |
* | Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome d'ext... | letouzey | 2006-06-05 |
* | Ajout exists! et restructuration/extension des fichiers sur la | herbelin | 2006-06-04 |
* | ajout de QArith dans les theories standards | letouzey | 2006-05-31 |
* | un debut de propriétés concernant FMap | letouzey | 2006-05-22 |
* | Dépendances pour List.v | notin | 2006-05-18 |
* | etoffage des notions de permutations (a la fois List.Permutation et Permutati... | letouzey | 2006-05-16 |
* | ajout de theories/FSets/DecidableTypeEx.v | letouzey | 2006-05-15 |
* | ajout d'exemples de decidable types | letouzey | 2006-05-15 |
* | Duplication du fichier FSetProperties pour les ensembles Weak. | letouzey | 2006-05-11 |
* | Cleanning and factorizing code in funind. Spliting new_arg_principles into to... | jforest | 2006-05-03 |
* | suite de l'ajout des FSets/FMaps dans les theories standards | letouzey | 2006-04-29 |
* | Régénération après mise à jour coqdep pour traiter Require multiple | herbelin | 2006-04-26 |
* | Un gros coup de lifting pour IntMap: | letouzey | 2006-04-25 |
* | versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes | letouzey | 2006-04-06 |
* | reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere... | letouzey | 2006-03-28 |
* | ajout d'un debut de proprietes pour les FSetWeak | letouzey | 2006-03-17 |
* | Ajout de theories/FSets contenant la partie "light" de FSets et FMap: | letouzey | 2006-03-15 |
* | Modularisation des preuves concernant la logique classique, l'indiscernabilit... | herbelin | 2006-03-05 |
* | maj | coq | 2006-02-22 |
* | Zmax et Zminmax | herbelin | 2006-02-12 |
* | maj | coq | 2006-02-09 |
* | maj | coq | 2006-02-08 |
* | maj | coq | 2005-11-18 |
* | maj | coq | 2005-11-07 |
* | new congruence | corbinea | 2005-08-17 |
* | reflexive tauto | corbinea | 2005-07-15 |
* | maj | coq | 2005-02-21 |
* | Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs | herbelin | 2005-02-03 |