aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool
Commit message (Expand)AuthorAge
* Numbers: finish files NStrongRec and NDefOpsGravatar letouzey2009-11-06
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
* - Correction bug highlighting "Module" dans CoqideGravatar herbelin2008-05-28
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* No compatibility notations for andb and co (this restore a correct Print output)Gravatar letouzey2008-04-17
* Prevent the apparition of &&& when printing a (if ... then ... else false)Gravatar letouzey2008-04-17
* - notations &&& and ||| equivalent to andb and orb, Gravatar letouzey2008-03-27
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* Major revision of FSetAVL: more Function, including some non-structural onesGravatar letouzey2008-02-09
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
* Big reorganization of romega/ReflOmegaCore.v: towards a modular Gravatar letouzey2007-07-10
* Compatibilité des noms longs de Bool déplacés dans DatatypesGravatar herbelin2007-07-03
* Déplacement des opérations sur bool dans l'état initialGravatar herbelin2007-04-28
* Noms "canoniques" pour certaines des propriétés de xor.Gravatar herbelin2006-10-17
* Mise en forme des theoriesGravatar notin2006-10-17
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* 2-3 lemmes en plus pour que les Bvectors soient effectivement utilisablesGravatar letouzey2006-04-27
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* Nettoyage Bool:Gravatar herbelin2006-02-12
* Ajout décidabilitéGravatar herbelin2006-01-31
* Fix sumbool_not hint (on behalf of cpaulin).Gravatar coq2005-07-15
* MAJ PolyList -> ListGravatar herbelin2005-03-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...Gravatar herbelin2004-03-28
* Ajout delimiteur pour bool_scopeGravatar herbelin2004-02-12
* backtrack implicit dans BvectorGravatar marche2004-02-10
* patch Bvector: args implicitesGravatar marche2004-02-09
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...Gravatar herbelin2003-11-01
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
* Syntax errorGravatar herbelin2003-10-16
* Suppression des surcharge de regles de grammaire en v7Gravatar herbelin2003-10-16
* Cacher les .v8Gravatar herbelin2003-10-03
* 'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...Gravatar herbelin2003-09-26
* Passage de Destruct a NewDestruct; '-' pour negbGravatar herbelin2003-09-26
* Remplacement de Induction/Destruct par NewInduction/NewDestructGravatar herbelin2003-09-23
* FSets, mais pas compile' par make worldGravatar filliatr2003-06-13
* Import nat_scopeGravatar herbelin2003-06-10
* Ne pas mettre d'associatif a droite au niveau 3 en V7Gravatar herbelin2003-05-29
* NotationsGravatar herbelin2003-05-21
* NotationsGravatar herbelin2003-04-29
* DefinedGravatar herbelin2003-04-09
* bit vectorsGravatar filliatr2003-01-06
* Making the sumbool functions transparent, so that they can used toGravatar bertot2002-07-09
* ZArith_base, Zbool, Bool_natGravatar filliatr2002-06-20