aboutsummaryrefslogtreecommitdiff
path: root/contrib/setoid_ring/Field_tac.v
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-18fixed ring/field warning about hyp cleaning upbarras
2009-03-17- gros commit sur ring et field: passage des arguments simplifiebarras
2008-04-29Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laherbelin
2007-02-05changement dans ring specification du sign, divisionbgregoir
2007-02-02field: introduction de Get_goalbgregoir
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-10generalisation de ring pour faire Ring_nfbarras
2006-10-30fixed field_simplify + changed precedence of let and fun in ltacbarras
2006-10-27simplif de la partie ML de ring/fieldbarras
2006-10-17field_simplify_eq profite de la factorisation de Laurentbarras
2006-10-10make sure BinList is not made visible to files that use the tactic Ringbertot
2006-10-04inefficacite de field_simplify_eqbarras
2006-10-02bug dans field_simplifybarras
2006-09-29args implicites dans Fieldbarras
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-26commit de field + renommagesbarras