| Age | Commit message (Expand) | Author |
|---|
| 2010-02-17 | Kill some useless dependencies (Bvector, Program.Syntax) | letouzey |
| 2010-02-10 | Euclidean division for NArith | letouzey |
| 2010-02-09 | Numbers: properties of min/max with respect to 0,S,P,add,sub,mul | letouzey |
| 2010-02-09 | NBinary improved, contains more, subsumes NOrderedType | letouzey |
| 2010-01-07 | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | letouzey |
| 2010-01-07 | Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni... | letouzey |
| 2010-01-07 | OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with... | letouzey |
| 2009-12-17 | Reverse order of arguments in min_case_strong for better uniformity (and comp... | letouzey |
| 2009-12-09 | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey |
| 2009-11-16 | Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms | letouzey |
| 2009-11-11 | Better compatibility for Peqb | letouzey |
| 2009-11-10 | DecidableType: A specification via boolean equality as an alternative to eq_dec | letouzey |
| 2009-11-03 | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey |
| 2009-11-03 | OrderedType implementation for various numerical datatypes + min/max structures | letouzey |
| 2009-11-02 | Remove various useless {struct} annotations | letouzey |
| 2009-10-08 | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey |
| 2009-09-28 | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-07-24 | OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith | letouzey |
| 2009-07-22 | Better comparison functions in OrderedTypeEx | letouzey |
| 2009-06-07 | - Added two new introduction patterns with the following temptative syntaxes: | herbelin |
| 2009-03-27 | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey |
| 2009-01-02 | - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H", | herbelin |
| 2008-12-28 | - Another bug in get_sort_family_of (sort-polymorphism of constants and | herbelin |
| 2008-10-26 | Fixes and refinements regarding occurrence selection: | herbelin |
| 2008-10-18 | Expérience de simplification de Ndigits compte tenu des tactiques existant | herbelin |
| 2008-06-01 | Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in | letouzey |
| 2008-04-16 | Definition of N moves back to BinNat (partial backtrack of commits 10298-10300) | letouzey |
| 2008-04-14 | BinPos: New version of ~1 and ~0 notations, xH replaced by 1 and proofs cleanup | letouzey |
| 2008-04-04 | - Amélioration de la présentation de RIneq, même si un nettoyage des | herbelin |
| 2008-03-07 | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau |
| 2008-02-10 | Proposal of a nice notation for constructors xI and xO of type positive | letouzey |
| 2007-11-08 | Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic. | emakarov |
| 2007-11-08 | setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. | letouzey |
| 2007-11-07 | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10300 85f007b7-540e-0... | emakarov |
| 2007-11-07 | Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v. | emakarov |
| 2007-11-07 | Replaced BinNat with a new version that is based on theories/Numbers/Natural/... | emakarov |
| 2007-11-01 | In agreement with Laurent Thery, start migration of auxiliary results | letouzey |
| 2007-10-16 | Added transitivity and irreflexivity of <, as well as < -elimination for bina... | emakarov |
| 2007-10-01 | Added the compilation of theories/Numbers to Makefile.common. The following t... | emakarov |
| 2007-09-20 | Changed the definition of Nminus in BinNat.v by removing comparison. | emakarov |
| 2007-07-18 | A generic preprocessing tactic zify for (r)omega | letouzey |
| 2007-06-07 | Extension of NArith: Nminus, Nmin, etc | letouzey |
| 2007-04-02 | Réparation de NArith/BinPos.v suite au commit #9739 | notin |
| 2007-03-30 | Added the following theorems to BinPos: | emakarov |
| 2007-03-14 | Removed an unnecessary argument (p : positive) in Prect_base. | emakarov |
| 2006-12-28 | Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à | herbelin |
| 2006-12-28 | Remplacement de la définition de Pind et Prec par une définition | herbelin |
| 2006-12-15 | Changement dans ring et field, beaucoup de correction d'erreurs, | bgregoir |
| 2006-10-05 | Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom | barras |
