| Age | Commit message (Expand) | Author |
|---|
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
| 2009-03-18 | fixed ring/field warning about hyp cleaning up | barras |
| 2009-03-17 | - gros commit sur ring et field: passage des arguments simplifie | barras |
| 2009-03-16 | Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4" | herbelin |
| 2009-03-14 | Makefile: ml dependencies of contribs are moved to .mllib files | letouzey |
| 2009-01-18 | Getting rid of the previous implementation of setoid_rewrite which was | msozeau |
| 2008-12-16 | Take advantage of natdynlink when available: almost all contribs become loada... | letouzey |
| 2008-10-26 | Fixes and refinements regarding occurrence selection: | herbelin |
| 2008-09-03 | Fix bug #1935, reworking the reflexivity, symmetry... tactics to use | msozeau |
| 2008-08-27 | Major speed and space improvements in setoid rewrite: | msozeau |
| 2008-08-05 | Correction de bugs: | herbelin |
| 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-27 | Enhanced discrimination nets implementation, which can now work with | msozeau |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-05-21 | refined the conversion oracle | barras |
| 2008-05-09 | Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ] | herbelin |
| 2008-05-01 | Clarification de l'ordre d'interprétation des variables dans ltac. En | herbelin |
| 2008-04-29 | Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la | herbelin |
| 2008-04-08 | - A little cleanup in Classes/*. Separate standard morphisms on | msozeau |
| 2008-03-16 | Removed unneeded tactics from RelationClasses. Use | msozeau |
| 2008-03-16 | Minor fixes on setoid rewriting. Now uses definitions of [relation] and | msozeau |
| 2008-03-07 | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau |
| 2008-03-06 | Plug the new setoid implemtation in, leaving the original one commented | msozeau |
| 2008-02-18 | Petite correction suite à la révision 10571 | notin |
| 2008-02-09 | Solde de code mort et petites optimisations sur lesquels je suis | herbelin |
| 2008-02-01 | Unification de TacLetRecIn et TacLetIn. En particulier, on peut | herbelin |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-11-08 | 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-07 | Replaced BinNat with a new version that is based on theories/Numbers/Natural/... | emakarov |
| 2007-09-20 | Changed the definition of Nminus in BinNat.v by removing comparison. | emakarov |
| 2007-09-17 | Raffinement de l'algorithme d'inférence de type | herbelin |
| 2007-07-24 | fixed bug 1448 and 1674 | barras |
| 2007-07-24 | fixed bug 1675: computing carrier from the relation type was not right | barras |
| 2007-07-12 | normalisation (by closure) was not performed under fixpoints | barras |
| 2007-07-12 | port de r9968: bug avec les ring calculatoires | barras |
| 2007-06-07 | Extension of NArith: Nminus, Nmin, etc | letouzey |
| 2007-04-29 | Orthographe en passant | herbelin |
| 2007-02-07 | doc de ring/field + option infinite -> completeness | barras |
| 2007-02-05 | changement dans ring specification du sign, division | bgregoir |
| 2007-02-02 | 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-01-24 | changement de la fonction norm_subst | bgregoir |
| 2007-01-23 | ring : Correction du bug PR#1306 | bgregoir |
| 2006-12-15 | Changement dans ring et field, beaucoup de correction d'erreurs, | bgregoir |
| 2006-12-11 | Changement dans le kernel : | bgregoir |
| 2006-11-16 | pb avec r9379 + modifs dans ring | barras |
| 2006-11-16 | suite de r9362: reconnaissance de qqs injections entre nat, N et Z | barras |
