| Commit message (Expand) | Author | Age |
|---|
| * | Fix bug #1935, reworking the reflexivity, symmetry... tactics to use |  msozeau | 2008-09-03 |
| * | Major speed and space improvements in setoid rewrite: | msozeau | 2008-08-27 |
| * | Correction de bugs: |  herbelin | 2008-08-05 |
| * | 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 |
| * | Enhanced discrimination nets implementation, which can now work with | msozeau | 2008-06-27 |
| * | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin | 2008-06-10 |
| * | refined the conversion oracle |  barras | 2008-05-21 |
| * | Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ] | herbelin | 2008-05-09 |
| * | Clarification de l'ordre d'interprétation des variables dans ltac. En | herbelin | 2008-05-01 |
| * | Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la | herbelin | 2008-04-29 |
| * | - A little cleanup in Classes/*. Separate standard morphisms on | msozeau | 2008-04-08 |
| * | Removed unneeded tactics from RelationClasses. Use | msozeau | 2008-03-16 |
| * | Minor fixes on setoid rewriting. Now uses definitions of [relation] and | msozeau | 2008-03-16 |
| * | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau | 2008-03-07 |
| * | Plug the new setoid implemtation in, leaving the original one commented | msozeau | 2008-03-06 |
| * | Petite correction suite à la révision 10571 |  notin | 2008-02-18 |
| * | Solde de code mort et petites optimisations sur lesquels je suis | herbelin | 2008-02-09 |
| * | Unification de TacLetRecIn et TacLetIn. En particulier, on peut | herbelin | 2008-02-01 |
| * | Factorisation des opérations sur le type option de Util dans un module |  aspiwack | 2007-12-05 |
| * | Prise en compte des notations "alias" dans la globalisation des coercions. | herbelin | 2007-11-08 |
| * | setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. | letouzey | 2007-11-08 |
| * | Replaced BinNat with a new version that is based on theories/Numbers/Natural/... |  emakarov | 2007-11-07 |
| * | Changed the definition of Nminus in BinNat.v by removing comparison. | emakarov | 2007-09-20 |
| * | Raffinement de l'algorithme d'inférence de type | herbelin | 2007-09-17 |
| * | fixed bug 1448 and 1674 | barras | 2007-07-24 |
| * | fixed bug 1675: computing carrier from the relation type was not right | barras | 2007-07-24 |
| * | normalisation (by closure) was not performed under fixpoints | barras | 2007-07-12 |
| * | port de r9968: bug avec les ring calculatoires | barras | 2007-07-12 |
| * | Extension of NArith: Nminus, Nmin, etc | letouzey | 2007-06-07 |
| * | Orthographe en passant | herbelin | 2007-04-29 |
| * | doc de ring/field + option infinite -> completeness | barras | 2007-02-07 |
| * | changement dans ring specification du sign, division |  bgregoir | 2007-02-05 |
| * | field: introduction de Get_goal | bgregoir | 2007-02-02 |
| * | ring: introduction de Get_goal | bgregoir | 2007-02-02 |
| * | Now 1/x * x simplifies to 1 |  thery | 2007-02-02 |
| * | changement de la fonction norm_subst | bgregoir | 2007-01-24 |
| * | ring : Correction du bug PR#1306 | bgregoir | 2007-01-23 |
| * | Changement dans ring et field, beaucoup de correction d'erreurs, | bgregoir | 2006-12-15 |
| * | Changement dans le kernel : | bgregoir | 2006-12-11 |
| * | pb avec r9379 + modifs dans ring | barras | 2006-11-16 |
| * | suite de r9362: reconnaissance de qqs injections entre nat, N et Z | barras | 2006-11-16 |
| * | generalisation de ring pour faire Ring_nf | barras | 2006-11-10 |
| * | fixed field_simplify + changed precedence of let and fun in ltac | barras | 2006-10-30 |
| * | Exports manquants dans ring | barras | 2006-10-29 |
| * | simplif de la partie ML de ring/field | barras | 2006-10-27 |
| * | changement des _sym par _comm dans setoid_ring | bgregoir | 2006-10-27 |
| * | Déplacement des propriétés générales de BinList dans List et des tactiqu... | herbelin | 2006-10-26 |
| * | field_simplify_eq profite de la factorisation de Laurent | barras | 2006-10-17 |
| * | changes the use of lists and notations, to avoid that the notations |  bertot | 2006-10-16 |
msozeau
herbelin
letouzey
barras
notin
aspiwack
emakarov
bgregoir
thery
bertot