aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zcomplements.v
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Gravatar Hugo Herbelin2014-10-17
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
* Testing a replacement of "cut" by "enough" on a couple of test files.Gravatar Hugo Herbelin2014-08-05
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* 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
* Some cleanup of ZcomplementsGravatar letouzey2011-07-01
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* one more substitution s/Set/Type/Gravatar letouzey2008-03-04
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* Mise en forme des theoriesGravatar notin2006-10-17
* revert, the previous commit was a mistakeGravatar bertot2006-10-05
* A version of natprering that should be more efficient and removal of a badGravatar bertot2006-10-05
* commit de field + renommagesGravatar barras2006-09-26
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Renoncement de la compatibilite des noms qualifies au profit de la compatibil...Gravatar herbelin2003-11-24
* CompatibiliteGravatar herbelin2003-11-22
* Bug implicit argumentsGravatar herbelin2003-11-14
* Restructuration ZArithGravatar herbelin2003-11-12
* Oubli d'un Set Implicit ArgumentsGravatar herbelin2003-11-07
* Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...Gravatar herbelin2003-11-05
* Documentation/StructurationGravatar herbelin2003-10-22
* Conflit de nom Pplus dans positive et dans polynomial (de ring)Gravatar herbelin2003-09-21
* Un peu d'aide pour le traducteurGravatar herbelin2003-08-10
* Arguments superflus pour Zlength_nilGravatar herbelin2003-06-18
* quelques adaptations de Zarith en vu de la nouvelle librarie FSetGravatar letouzey2003-06-13
* Ajout Open ScopeGravatar herbelin2003-04-09
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".Gravatar herbelin2003-04-09
* *** empty log message ***Gravatar barras2003-03-12
* ZArith_base, Zbool, Bool_natGravatar filliatr2002-06-20
* affaiblissement hyp de Zmult_reg_leftGravatar filliatr2002-06-05
* encore des lemmes sur ZdivGravatar filliatr2002-05-14
* nouveaux lemmes dans Zdiv (Claude Marche)Gravatar filliatr2002-05-14
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* nouveau module ZdivGravatar filliatr2002-04-05
* petits changements afin de profiter du nouveau Rewrite/inGravatar barras2002-03-05
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* Zdiv et Zmod dans ZcomplementsGravatar filliatr2002-01-25
* amadouage de coqwebGravatar letouzey2002-01-18
* ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...Gravatar letouzey2002-01-18