| Commit message (Expand) | Author | Age |
* | Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358. | herbelin | 2009-10-04 |
* | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey | 2009-09-28 |
* | Add a few properties about Rmin/Rmax with replication in Zmin/Zmax. | herbelin | 2009-09-27 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey | 2009-09-09 |
* | Fixed extra space in printing notation { x & P } + minor other things | herbelin | 2009-08-11 |
* | 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-07-24 |
* | - Added two new introduction patterns with the following temptative syntaxes: | herbelin | 2009-06-07 |
* | adds a theorem to reason at the level of Z | bertot | 2009-05-07 |
* | Some additions in Max and Zmax. Unifiying list of statements and names | herbelin | 2009-04-14 |
* | ZArith/Int: no need to load romega here (but rather in FullAVL) | letouzey | 2009-03-28 |
* | - Added support for subterm matching in SearchAbout. | herbelin | 2008-12-29 |
* | Zdiv: eqm (equality modulo some N) can now be declared as Parametric Relation | letouzey | 2008-10-20 |
* | Tauto breaking not only binary "conjunctions" seems like a bad idea | msozeau | 2008-07-24 |
* | Oops... forgot some debug code. | msozeau | 2008-07-23 |
* | A try at allowing matching on applications as a binary syntax node by default. | msozeau | 2008-07-22 |
* | Fix bug #1899: no more strange notations for Qge and Qgt | letouzey | 2008-07-04 |
* | Zpow_facts.Zmult_power: kills a useless hypothesis | letouzey | 2008-06-11 |
* | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
* | - Modification de la déf de minus et pred conformément aux remarques de | herbelin | 2008-05-28 |
* | Cyclic31: migrate auxiliary lemmas to their legitimate files | letouzey | 2008-05-27 |
* | Cyclic31 : proof of the spec of gcd31 | letouzey | 2008-05-27 |
* | switch theories/Numbers from Set to Type (both the abstract and the bignum pa... | letouzey | 2008-05-22 |
* | - Changement du code de Zplus pour accomoder ring qui sinon prend une | herbelin | 2008-05-11 |
* | Backtrack on using metas eagerly in auto, only done in "new auto" for | msozeau | 2008-04-28 |
* | - Fix bug in unification not taking into account the right meta | msozeau | 2008-04-27 |
* | Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression | notin | 2008-03-28 |
* | Fix bugs that were reopened due to the change of setoid | msozeau | 2008-03-08 |
* | Plug the new setoid implemtation in, leaving the original one commented | msozeau | 2008-03-06 |
* | one more substitution s/Set/Type/ | letouzey | 2008-03-04 |
* | Proposal of a nice notation for constructors xI and xO of type positive | letouzey | 2008-02-10 |
* | one forgotten compatibility lemma | letouzey | 2008-02-08 |
* | Keep the Z_scope local to this file. | roconnor | 2008-01-24 |
* | Adding Zdiv_le_compat_l | thery | 2008-01-22 |
* | A result about Zsgn(a/b), both for Zdiv and ZOdiv | letouzey | 2007-11-10 |
* | First reasonably complete version of ZOdiv, including some properties | letouzey | 2007-11-10 |
* | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0... | jforest | 2007-11-09 |
* | more about ZOdiv and ZOmod (still not finished) | letouzey | 2007-11-09 |
* | setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. | letouzey | 2007-11-08 |
* | small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is | letouzey | 2007-11-06 |
* | Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of... | letouzey | 2007-11-06 |
* | Adding Qround.v (and helper lemmas and hints) | roconnor | 2007-11-01 |
* | In agreement with Laurent Thery, start migration of auxiliary results | letouzey | 2007-11-01 |
* | Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le | roconnor | 2007-10-19 |
* | Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.v | emakarov | 2007-08-08 |
* | A generic preprocessing tactic zify for (r)omega | letouzey | 2007-07-18 |
* | normalisation (by closure) was not performed under fixpoints | barras | 2007-07-12 |
* | Transparency of Z_lt_le_dec | notin | 2007-04-12 |
* | Bug nommage Zgt_trans_succ | herbelin | 2006-12-12 |