| Age | Commit message (Expand) | Author |
|---|
| 2011-11-03 | Cleaning a little bit the files talking about descriptions: avoiding | herbelin |
| 2011-05-05 | BinInt: Z.add become the alternative Z.add' | letouzey |
| 2011-04-13 | - Improve unification (beta-reduction, and same heuristic as evarconv for red... | msozeau |
| 2011-04-13 | Fix scripts relying on unification not doing any beta reduction. | msozeau |
| 2011-04-13 | Unify meta types with the right flags, add betaiotazeta reduction to unificat... | msozeau |
| 2011-03-17 | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-12-10 | First release of Vector library. | pboutill |
| 2010-11-18 | Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits | letouzey |
| 2010-10-21 | Solve name conflict about pow introduced by commit 13546. | letouzey |
| 2010-10-14 | Numbers: new functions pow, even, odd + many reorganisations | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-02-18 | Removed redundant and ill-named technical lemma. | gmelquio |
| 2010-02-18 | Removed SeqProp's dependency on Classical. | gmelquio |
| 2010-02-18 | Removed Rtrigo's dependency on Classical. | gmelquio |
| 2010-02-17 | Removed Rseries' dependency on Classical. | gmelquio |
| 2010-02-17 | Removed Rlimit's dependency on Classical. | gmelquio |
| 2010-02-17 | Removed Rderiv's dependency on Classical. | gmelquio |
| 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-12-06 | Fix anomaly when using typeclass resolution with filtered hyps in evars. | msozeau |
| 2009-11-16 | Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms | letouzey |
| 2009-11-10 | DecidableType: A specification via boolean equality as an alternative to eq_dec | letouzey |
| 2009-11-03 | ROrderedType + Rminmax : Coq's Reals can be seen as OrderedType. | letouzey |
| 2009-11-02 | Remove various useless {struct} annotations | letouzey |
| 2009-11-02 | Added alternate versions of existing lemmas on sqrt. | gmelquio |
| 2009-10-08 | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey |
| 2009-10-04 | Removal of trailing spaces. | serpyc |
| 2009-10-04 | Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358. | herbelin |
| 2009-09-28 | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey |
| 2009-09-27 | Add a few properties about Rmin/Rmax with replication in Zmin/Zmax. | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-11 | Added the following lemmas to homogenize Reals a bit: | gmelquio |
| 2009-03-27 | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey |
| 2009-03-17 | - gros commit sur ring et field: passage des arguments simplifie | barras |
| 2009-02-06 | Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2] | herbelin |
| 2008-12-16 | Take advantage of natdynlink when available: almost all contribs become loada... | letouzey |
| 2008-05-12 | MAJ et bricoles diverses | herbelin |
| 2008-04-06 | Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt : | herbelin |
| 2008-04-05 | Suite 10760 | herbelin |
| 2008-04-05 | - Retour en arrière sur la capacité du nouvel apply à utiliser les | herbelin |
| 2008-04-04 | - Amélioration de la présentation de RIneq, même si un nettoyage des | herbelin |
| 2008-03-23 | Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards. | herbelin |
| 2008-03-23 | Une passe sur les réels: | herbelin |
| 2008-03-01 | Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_O | herbelin |
