aboutsummaryrefslogtreecommitdiff
path: root/contrib/setoid_ring
AgeCommit message (Expand)Author
2007-06-07Extension of NArith: Nminus, Nmin, etcletouzey
2007-04-29Orthographe en passantherbelin
2007-02-07doc de ring/field + option infinite -> completenessbarras
2007-02-05changement dans ring specification du sign, divisionbgregoir
2007-02-02field: introduction de Get_goalbgregoir
2007-02-02ring: introduction de Get_goalbgregoir
2007-02-02Now 1/x * x simplifies to 1thery
2007-01-24changement de la fonction norm_substbgregoir
2007-01-23ring : Correction du bug PR#1306bgregoir
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
2006-12-11Changement dans le kernel : bgregoir
2006-11-16pb avec r9379 + modifs dans ringbarras
2006-11-16suite de r9362: reconnaissance de qqs injections entre nat, N et Zbarras
2006-11-10generalisation de ring pour faire Ring_nfbarras
2006-10-30fixed field_simplify + changed precedence of let and fun in ltacbarras
2006-10-29Exports manquants dans ringbarras
2006-10-27simplif de la partie ML de ring/fieldbarras
2006-10-27changement des _sym par _comm dans setoid_ringbgregoir
2006-10-26Déplacement des propriétés générales de BinList dans List et des tactiqu...herbelin
2006-10-17field_simplify_eq profite de la factorisation de Laurentbarras
2006-10-16changes the use of lists and notations, to avoid that the notationsbertot
2006-10-12Fix name clash on leftthery
2006-10-10Remove duplicate conditions in Field + Monomial substitution function for PExprthery
2006-10-10make sure BinList is not made visible to files that use the tactic Ringbertot
2006-10-05A version of natprering that should be more efficient and removal of a badbertot
2006-10-05Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynombarras
2006-10-05Corrects the problem described in PR#1240:bertot
2006-10-04inefficacite de field_simplify_eqbarras
2006-10-02bug dans field_simplifybarras
2006-09-29args implicites dans Fieldbarras
2006-09-29git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9188 85f007b7-540e-04...barras
2006-09-28separation de RealFieldbarras
2006-09-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 85f007b7-540e-04...barras
2006-09-26Compilation newringnotin
2006-09-26commit de field + renommagesbarras
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...herbelin
2006-02-01protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)barras
2006-02-01protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)barras
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-18petites corrections + contournement bug projectionsbarras
2005-11-18commited first version of new ringbarras