aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool/Bool.v
Commit message (Expand)AuthorAge
* Updating headers.Gravatar herbelin2012-08-08
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Follow-up concerning eqb / ltb / leb comparisonsGravatar letouzey2011-06-21
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Bool: shorter and more systematic proofs + an iff lemma about eqbGravatar letouzey2010-07-16
* Bool: iff lemmas about or, a reflect inductive, an is_true functionGravatar letouzey2010-07-10
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Numbers: finish files NStrongRec and NDefOpsGravatar letouzey2009-11-06
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
* 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
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* Nettoyage Bool:Gravatar herbelin2006-02-12
* Ajout décidabilitéGravatar herbelin2006-01-31
* Nouvelle en-têteGravatar herbelin2004-07-16
* Ajout delimiteur pour bool_scopeGravatar herbelin2004-02-12
* 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
* '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
* FSets, mais pas compile' par make worldGravatar filliatr2003-06-13
* Ne pas mettre d'associatif a droite au niveau 3 en V7Gravatar herbelin2003-05-29
* NotationsGravatar herbelin2003-05-21
* NotationsGravatar herbelin2003-04-29
* Making the sumbool functions transparent, so that they can used toGravatar bertot2002-07-09
* StandardisationGravatar herbelin2002-05-06
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
* Ajout andb_true_eq pour PolyList.list_beqGravatar herbelin2002-02-28
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* Simplification de deux preuves. En outre ca simplifie leur extraction.Gravatar letouzey2001-09-27
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
* Mise de (*i autour CVS infoGravatar mohring2001-04-19
* Ajout de lemmes sur les booleensGravatar mohring2001-03-30