aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/Zcomplements.v
AgeCommit message (Expand)Author
2020-10-11Modify ZArith/Zcomplements.v to compile with -mangle-namesJasper Hugunin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-22Zcomplements: do not use “omega”Vincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-10-17Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Hugo Herbelin
2014-10-17Essai où assert_style n'est utilisé que si pas visuellement une équation;Hugo Herbelin
2014-08-05Testing a replacement of "cut" by "enough" on a couple of test files.Hugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-07-01Some cleanup of Zcomplementsletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-02Remove various useless {struct} annotationsletouzey
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-03-04one more substitution s/Set/Type/letouzey
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
2006-10-17Mise en forme des theoriesnotin
2006-10-05revert, the previous commit was a mistakebertot
2006-10-05A version of natprering that should be more efficient and removal of a badbertot
2006-09-26commit de field + renommagesbarras
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2004-07-16Nouvelle en-têteherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-24Renoncement de la compatibilite des noms qualifies au profit de la compatibil...herbelin
2003-11-22Compatibiliteherbelin
2003-11-14Bug implicit argumentsherbelin
2003-11-12Restructuration ZArithherbelin
2003-11-07Oubli d'un Set Implicit Argumentsherbelin
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...herbelin
2003-10-22Documentation/Structurationherbelin
2003-09-21Conflit de nom Pplus dans positive et dans polynomial (de ring)herbelin
2003-08-10Un peu d'aide pour le traducteurherbelin
2003-06-18Arguments superflus pour Zlength_nilherbelin
2003-06-13quelques adaptations de Zarith en vu de la nouvelle librarie FSetletouzey
2003-04-09Ajout Open Scopeherbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
2003-03-12*** empty log message ***barras
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2002-06-05affaiblissement hyp de Zmult_reg_leftfilliatr
2002-05-14encore des lemmes sur Zdivfilliatr
2002-05-14nouveaux lemmes dans Zdiv (Claude Marche)filliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:16:57 +0000