| Commit message (Expand) | Author | Age |
* | Remove v62 from stdlib. | Théo Zimmermann | 2016-10-24 |
* | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Fixing typo absorption (bug #3751). | Hugo Herbelin | 2014-10-22 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey | 2012-07-05 |
* | ZArith + other : favor the use of modern names instead of compat notations | letouzey | 2012-07-05 |
* | Follow-up concerning eqb / ltb / leb comparisons | letouzey | 2011-06-21 |
* | Numbers and bitwise functions. | letouzey | 2010-12-06 |
* | Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits | letouzey | 2010-11-18 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Bool: shorter and more systematic proofs + an iff lemma about eqb | letouzey | 2010-07-16 |
* | Bool: iff lemmas about or, a reflect inductive, an is_true function | letouzey | 2010-07-10 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Numbers: finish files NStrongRec and NDefOps | letouzey | 2009-11-06 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey | 2009-09-09 |
* | No compatibility notations for andb and co (this restore a correct Print output) | letouzey | 2008-04-17 |
* | Prevent the apparition of &&& when printing a (if ... then ... else false) | letouzey | 2008-04-17 |
* | - notations &&& and ||| equivalent to andb and orb, | letouzey | 2008-03-27 |
* | migration from Set to Type of FSet/FMap + some dependencies... | letouzey | 2008-03-04 |
* | Major revision of FSetAVL: more Function, including some non-structural ones | letouzey | 2008-02-09 |
* | Added the automatic generation of the boolean equality if possible and the | vsiles | 2007-10-05 |
* | Big reorganization of romega/ReflOmegaCore.v: towards a modular | letouzey | 2007-07-10 |
* | Compatibilité des noms longs de Bool déplacés dans Datatypes | herbelin | 2007-07-03 |
* | Déplacement des opérations sur bool dans l'état initial | herbelin | 2007-04-28 |
* | Noms "canoniques" pour certaines des propriétés de xor. | herbelin | 2006-10-17 |
* | Mise en forme des theories | notin | 2006-10-17 |
* | Modification des propriétés (svn:executable) | notin | 2006-03-17 |
* | Nettoyage Bool: | herbelin | 2006-02-12 |
* | Ajout décidabilité | herbelin | 2006-01-31 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Ajout delimiteur pour bool_scope | herbelin | 2004-02-12 |
* | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin | 2003-11-29 |
* | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin | 2003-11-01 |
* | reorganisation des niveaux (ex: = est a 70) | barras | 2003-10-22 |
* | Syntax error | herbelin | 2003-10-16 |
* | Suppression des surcharge de regles de grammaire en v7 | herbelin | 2003-10-16 |
* | 'Open Local Scope' en attendant que le core_scope sache se mettre devant impl... | herbelin | 2003-09-26 |
* | Passage de Destruct a NewDestruct; '-' pour negb | herbelin | 2003-09-26 |
* | FSets, mais pas compile' par make world | filliatr | 2003-06-13 |
* | Ne pas mettre d'associatif a droite au niveau 3 en V7 | herbelin | 2003-05-29 |
* | Notations | herbelin | 2003-05-21 |
* | Notations | herbelin | 2003-04-29 |
* | Making the sumbool functions transparent, so that they can used to | bertot | 2002-07-09 |
* | Standardisation | herbelin | 2002-05-06 |
* | Uniformisation (Qed/Save et Implicits Arguments) | herbelin | 2002-04-17 |
* | Nouveau Rewrite-in plus economique | barras | 2002-03-04 |
* | Ajout andb_true_eq pour PolyList.list_beq | herbelin | 2002-02-28 |
* | option -dump-glob pour coqdoc | filliatr | 2002-02-14 |