aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool
Commit message (Expand)AuthorAge
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* 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
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Follow-up concerning eqb / ltb / leb comparisonsGravatar letouzey2011-06-21
* First release of Vector library.Gravatar pboutill2010-12-10
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
* Bvector.Vshiftin was wrong for agesGravatar pboutill2010-09-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* 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
* Kill some useless dependencies (Bvector, Program.Syntax)Gravatar letouzey2010-02-17
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* 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