aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
2009-01-27- Fixed various Overfull in documentation.herbelin
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-26- Optimized "auto decomp" which had a (presumably) exponential inherbelin
2008-12-17FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...letouzey
2008-12-16Move FunctionalExtensionality to Logic/ (someone please check that themsozeau
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-07-15Autour du parsing:herbelin
2008-06-10- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.herbelin
2008-04-04A file that can be loaded when a migration from Set to Type is desiredletouzey
2008-04-04Correction problème de compil (blast.ml)herbelin
2008-03-30Modifications diverses et variées :herbelin
2008-03-23Nettoyage Wf.v et unification (suite remarques faites sur cocorico)herbelin
2008-03-23Une passe sur les réels:herbelin
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
2008-02-02factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...letouzey
2008-01-23Changing R to a local definition so that it isn't exported.roconnor
2007-11-24* A few Parameter Inline, but they dont seem to help much concerning letouzey
2007-10-29Revision of the FSetWeak Interface, so that it becomes a precise letouzey
2007-10-03Révision de theories/Logic concernant les axiomes de descriptions.herbelin
2007-10-01Nouvelle mise à jourherbelin
2007-09-30Ajout infos de débogage de "universe inconsistency" quand option Setherbelin
2007-09-26 added a lemma to prove inj_pair2 when eq_dec is available.vsiles
2007-06-21Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, notin
2007-05-22Comparaison JMeq/eq_depherbelin
2007-04-25Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création herbelin
2007-03-15Typosherbelin
2007-02-06Passage de Set à Type dans Relations et Wellfoundedherbelin
2007-01-31Correction typo eq_rec_eq (cf bug #1339)herbelin
2007-01-23Derivation of (exists x : A, P x) -> {x : A | P x} for decidable Pemakarov
2007-01-22Clarification redondance Axiome du choix unique/descriptionherbelin
2006-12-28Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àherbelin
2006-12-12AllÃègement de syntxe suite à l'introduction de l'unif patternherbelin
2006-10-17Mise en forme des theoriesnotin
2006-08-28Passage à une définition de inhabited plus dans les 'standard mathématique...herbelin
2006-08-28"Essai de remplacement de "ex P" par "exists x, P x" suite àherbelin
2006-08-24JMeq maintenant applicable sur Typeherbelin
2006-07-06Typoherbelin
2006-07-04MAJ du manuel de référencenotin
2006-06-09Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...herbelin
2006-06-04Ajout exists! et restructuration/extension des fichiers sur laherbelin
2006-06-04Ajout exists! et restructuration/extension des fichiers sur laherbelin
2006-04-28Standardisation du nom des méthodes de Evdherbelin
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...notin
2006-03-30Réajout de eq_rec_eq oublié lors de la modularisation de Eqdepherbelin
2006-03-17Modification des propriétés (svn:executable)notin
2006-03-05Modularisation des preuves concernant la logique classique, l'indiscernabilit...herbelin
2006-03-05Commentairesherbelin
2006-03-05Renommage du IP classique pour éviter confusion avec IP constructifherbelin
2006-03-05Ajout étude IP généralisé, Gödel-Dummett, buveurherbelin
2006-03-04Petite simplification en passantherbelin