aboutsummaryrefslogtreecommitdiff
path: root/contrib/setoid_ring/Field_theory.v
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-17- gros commit sur ring et field: passage des arguments simplifiebarras
2008-07-22A try at allowing matching on applications as a binary syntax node by default.msozeau
2008-05-21refined the conversion oraclebarras
2008-03-07Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partmsozeau
2008-02-18Petite correction suite à la révision 10571notin
2007-11-07Replaced BinNat with a new version that is based on theories/Numbers/Natural/...emakarov
2007-04-29Orthographe en passantherbelin
2007-02-05changement dans ring specification du sign, divisionbgregoir
2007-02-02Now 1/x * x simplifies to 1thery
2007-01-24changement de la fonction norm_substbgregoir
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
2006-12-11Changement dans le kernel : bgregoir
2006-10-27simplif de la partie ML de ring/fieldbarras
2006-10-27changement des _sym par _comm dans setoid_ringbgregoir
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-02bug dans field_simplifybarras
2006-09-29args implicites dans Fieldbarras
2006-09-28separation de RealFieldbarras