| Age | Commit message (Expand) | Author |
|---|
| 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 | ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType | letouzey |
| 2010-01-17 | BigN, BigZ, BigQ: presentation via unique module with both ops and props | letouzey |
| 2010-01-14 | Rename Zbinary into Zdigit in order to avoid confusion with Numbers/.../ZBina... | letouzey |
| 2010-01-11 | Support "Local Obligation Tactic" (now the default in sections). | msozeau |
| 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 |
| 2010-01-05 | Numbers abstract layer: more Module Type, used especially for divisions. | letouzey |
| 2010-01-05 | Zdiv seen as a quasi-instantation of generic ZDivFloor from theories/Numbers | letouzey |
| 2009-12-17 | ZOdiv: fully use generic properties from ZDivTrunc.v | letouzey |
| 2009-12-17 | Reverse order of arguments in min_case_strong for better uniformity (and comp... | letouzey |
| 2009-12-17 | Division in Numbers : more properties, new filenames based on a paper by R. B... | letouzey |
| 2009-12-16 | Division in Numbers: more properties proved (still W.I.P.) | letouzey |
| 2009-12-15 | A generic euclidean division in Numbers (Still Work-In-Progress) | 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-10 | Simplification of Numbers, mainly thanks to Include | 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-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-09 | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey |
| 2009-08-11 | Fixed extra space in printing notation { x & P } + minor other things | herbelin |
| 2009-07-24 | OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith | letouzey |
| 2009-07-24 | Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite" | letouzey |
| 2009-06-07 | - Added two new introduction patterns with the following temptative syntaxes: | herbelin |
| 2009-05-07 | adds a theorem to reason at the level of Z | bertot |
| 2009-04-14 | Some additions in Max and Zmax. Unifiying list of statements and names | herbelin |
| 2009-03-28 | ZArith/Int: no need to load romega here (but rather in FullAVL) | letouzey |
| 2008-12-29 | - Added support for subterm matching in SearchAbout. | herbelin |
| 2008-10-20 | Zdiv: eqm (equality modulo some N) can now be declared as Parametric Relation | letouzey |
| 2008-07-24 | Tauto breaking not only binary "conjunctions" seems like a bad idea | msozeau |
| 2008-07-23 | Oops... forgot some debug code. | msozeau |
| 2008-07-22 | A try at allowing matching on applications as a binary syntax node by default. | msozeau |
| 2008-07-04 | Fix bug #1899: no more strange notations for Qge and Qgt | letouzey |
| 2008-06-11 | Zpow_facts.Zmult_power: kills a useless hypothesis | letouzey |
| 2008-06-08 | - Extension de "generalize" en "generalize c as id at occs". | herbelin |
| 2008-05-28 | - Modification de la déf de minus et pred conformément aux remarques de | herbelin |
| 2008-05-27 | Cyclic31: migrate auxiliary lemmas to their legitimate files | letouzey |
| 2008-05-27 | Cyclic31 : proof of the spec of gcd31 | letouzey |
| 2008-05-22 | switch theories/Numbers from Set to Type (both the abstract and the bignum pa... | letouzey |
| 2008-05-11 | - Changement du code de Zplus pour accomoder ring qui sinon prend une | herbelin |
| 2008-04-28 | Backtrack on using metas eagerly in auto, only done in "new auto" for | msozeau |
