aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/setoid_ring
Commit message (Expand)AuthorAge
* Fix bug #1935, reworking the reflexivity, symmetry... tactics to useGravatar msozeau2008-09-03
* Major speed and space improvements in setoid rewrite:Gravatar msozeau2008-08-27
* Correction de bugs:Gravatar herbelin2008-08-05
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
* Fix bug #1899: no more strange notations for Qge and QgtGravatar letouzey2008-07-04
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* refined the conversion oracleGravatar barras2008-05-21
* Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]Gravatar herbelin2008-05-09
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* Removed unneeded tactics from RelationClasses. UseGravatar msozeau2008-03-16
* Minor fixes on setoid rewriting. Now uses definitions of [relation] andGravatar msozeau2008-03-16
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Petite correction suite à la révision 10571Gravatar notin2008-02-18
* Solde de code mort et petites optimisations sur lesquels je suisGravatar herbelin2008-02-09
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
* setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. Gravatar letouzey2007-11-08
* Replaced BinNat with a new version that is based on theories/Numbers/Natural/...Gravatar emakarov2007-11-07
* Changed the definition of Nminus in BinNat.v by removing comparison.Gravatar emakarov2007-09-20
* Raffinement de l'algorithme d'inférence de typeGravatar herbelin2007-09-17
* fixed bug 1448 and 1674Gravatar barras2007-07-24
* fixed bug 1675: computing carrier from the relation type was not rightGravatar barras2007-07-24
* normalisation (by closure) was not performed under fixpointsGravatar barras2007-07-12
* port de r9968: bug avec les ring calculatoiresGravatar barras2007-07-12
* Extension of NArith: Nminus, Nmin, etcGravatar letouzey2007-06-07
* Orthographe en passantGravatar herbelin2007-04-29
* doc de ring/field + option infinite -> completenessGravatar barras2007-02-07
* changement dans ring specification du sign, divisionGravatar bgregoir2007-02-05
* field: introduction de Get_goalGravatar bgregoir2007-02-02
* ring: introduction de Get_goalGravatar bgregoir2007-02-02
* Now 1/x * x simplifies to 1Gravatar thery2007-02-02
* changement de la fonction norm_substGravatar bgregoir2007-01-24
* ring : Correction du bug PR#1306Gravatar bgregoir2007-01-23
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* pb avec r9379 + modifs dans ringGravatar barras2006-11-16
* suite de r9362: reconnaissance de qqs injections entre nat, N et ZGravatar barras2006-11-16
* generalisation de ring pour faire Ring_nfGravatar barras2006-11-10
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* Exports manquants dans ringGravatar barras2006-10-29
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
* Déplacement des propriétés générales de BinList dans List et des tactiqu...Gravatar herbelin2006-10-26
* field_simplify_eq profite de la factorisation de LaurentGravatar barras2006-10-17
* changes the use of lists and notations, to avoid that the notationsGravatar bertot2006-10-16