| Commit message (Expand) | Author | Age |
... | |
* | 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 |
* | correction Open Local Scope (Ring) | bgregoir | 2006-12-11 |
* | Changement dans le kernel : | bgregoir | 2006-12-11 |
* | fixed field_simplify + changed precedence of let and fun in ltac | barras | 2006-10-30 |
* | simplif de la partie ML de ring/field | barras | 2006-10-27 |
* | Mise en forme des theories | notin | 2006-10-17 |
* | revert, the previous commit was a mistake | bertot | 2006-10-05 |
* | A version of natprering that should be more efficient and removal of a bad | bertot | 2006-10-05 |
* | Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom | barras | 2006-10-05 |
* | commit de field + renommages | barras | 2006-09-26 |
* | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras | 2006-09-26 |
* | Ajout de Zgcd_spec (compat.) | notin | 2006-06-26 |
* | nouvel algorithme pour Zgcd (plus rapide) + un Qcompare | letouzey | 2006-06-25 |
* | Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT... | herbelin | 2006-06-09 |
* | ajout de QArith dans les theories standards | letouzey | 2006-05-31 |
* | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin | 2006-05-28 |
* | Changement de précédence de l'argument du by de assert; conséquences... | herbelin | 2006-05-23 |
* | On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_pos | letouzey | 2006-05-14 |
* | typo | letouzey | 2006-05-13 |
* | un Zgcd calculant dans coq | letouzey | 2006-05-13 |
* | une fonction pouvant calculer le gcd en coq | letouzey | 2006-05-11 |
* | un Zgcd general gardant trace des coefs | letouzey | 2006-05-05 |
* | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin | 2006-04-28 |
* | Bug Scope | herbelin | 2006-02-12 |
* | Nettoyage Zmin.v, création Zmax.v et Zminmax.v | herbelin | 2006-02-12 |
* | Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p... | herbelin | 2005-05-02 |
* | Lemme de passage de l'autre côté d'une égalité | herbelin | 2005-05-02 |
* | Fixed hypotheses of Z_lt_induction (see #957) | herbelin | 2005-04-26 |
* | Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h... | herbelin | 2005-03-29 |
* | Missing translating a 'O' into a '0' | herbelin | 2005-03-24 |
* | Changement dans les boxed values . | gregoire | 2004-11-12 |
* | 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval... | herbelin | 2004-10-11 |
* | Zbool déjà dans ZArith_base | herbelin | 2004-08-03 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | backtrack implicit dans Bvector | marche | 2004-02-10 |
* | patch Bvector: args implicites | marche | 2004-02-09 |
* | changement de pose en set (pose n'etait pas utilise avec la semantique | barras | 2003-12-24 |
* | Duplication temporaire des règles de syntaxe des paires | herbelin | 2003-12-16 |
* | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras | 2003-12-15 |
* | Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p... | herbelin | 2003-12-04 |
* | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin | 2003-11-29 |
* | ground->firstorder, cc-> congruence, CC final commit | corbinea | 2003-11-29 |
* | Report de lemmes de Znumtheory dans Zabs ou BinInt | herbelin | 2003-11-29 |
* | Renoncement de la compatibilite des noms qualifies au profit de la compatibil... | herbelin | 2003-11-24 |
* | Compatibilite | herbelin | 2003-11-22 |