aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith
Commit message (Expand)AuthorAge
...
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* 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
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
* Better comparison functions in OrderedTypeExGravatar letouzey2009-07-22
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Parsing files for numerals (+ ascii/string) moved into pluginsGravatar letouzey2009-03-27
* - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",Gravatar herbelin2009-01-02
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Expérience de simplification de Ndigits compte tenu des tactiques existantGravatar herbelin2008-10-18
* Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inGravatar letouzey2008-06-01
* Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)Gravatar letouzey2008-04-16
* BinPos: New version of ~1 and ~0 notations, xH replaced by 1 and proofs cleanupGravatar letouzey2008-04-14
* - Amélioration de la présentation de RIneq, même si un nettoyage desGravatar herbelin2008-04-04
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Proposal of a nice notation for constructors xI and xO of type positiveGravatar letouzey2008-02-10
* Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.Gravatar emakarov2007-11-08
* setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. Gravatar letouzey2007-11-08
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10300 85f007b7-540e-0...Gravatar emakarov2007-11-07
* Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v.Gravatar emakarov2007-11-07
* Replaced BinNat with a new version that is based on theories/Numbers/Natural/...Gravatar emakarov2007-11-07
* In agreement with Laurent Thery, start migration of auxiliary results Gravatar letouzey2007-11-01
* Added transitivity and irreflexivity of <, as well as < -elimination for bina...Gravatar emakarov2007-10-16
* Added the compilation of theories/Numbers to Makefile.common. The following t...Gravatar emakarov2007-10-01
* Changed the definition of Nminus in BinNat.v by removing comparison.Gravatar emakarov2007-09-20
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* Extension of NArith: Nminus, Nmin, etcGravatar letouzey2007-06-07
* Réparation de NArith/BinPos.v suite au commit #9739Gravatar notin2007-04-02
* Added the following theorems to BinPos:Gravatar emakarov2007-03-30
* Removed an unnecessary argument (p : positive) in Prect_base.Gravatar emakarov2007-03-14
* Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àGravatar herbelin2006-12-28
* Remplacement de la définition de Pind et Prec par une définitionGravatar herbelin2006-12-28
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
* Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynomGravatar barras2006-10-05
* qq proprietes de plus sur NcompareGravatar letouzey2006-04-29
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* suite du pont entre Bvector et NGravatar letouzey2006-04-26
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25
* ouverture du bon scope (positive_scope) derriere le constructeur Npos de NGravatar letouzey2006-04-06
* Minimum pour documentation TeX de la biblioGravatar herbelin2006-02-22
* Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des jours...Gravatar coq2005-02-07
* Suppression de l'Unboxed des opérations sur positive (cf bug 898)Gravatar herbelin2005-02-04
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Nouvelle en-têteGravatar herbelin2004-07-16
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-18 18:19:48 +0000