index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
setoid_ring
/
Field_theory.v
Age
Commit message (
Expand
)
Author
2009-03-20
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-17
- gros commit sur ring et field: passage des arguments simplifie
barras
2008-07-22
A try at allowing matching on applications as a binary syntax node by default.
msozeau
2008-05-21
refined the conversion oracle
barras
2008-03-07
Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part
msozeau
2008-02-18
Petite correction suite à la révision 10571
notin
2007-11-07
Replaced BinNat with a new version that is based on theories/Numbers/Natural/...
emakarov
2007-04-29
Orthographe en passant
herbelin
2007-02-05
changement dans ring specification du sign, division
bgregoir
2007-02-02
Now 1/x * x simplifies to 1
thery
2007-01-24
changement de la fonction norm_subst
bgregoir
2006-12-15
Changement dans ring et field, beaucoup de correction d'erreurs,
bgregoir
2006-12-11
Changement dans le kernel :
bgregoir
2006-10-27
simplif de la partie ML de ring/field
barras
2006-10-27
changement des _sym par _comm dans setoid_ring
bgregoir
2006-10-17
field_simplify_eq profite de la factorisation de Laurent
barras
2006-10-16
changes the use of lists and notations, to avoid that the notations
bertot
2006-10-12
Fix name clash on left
thery
2006-10-10
Remove duplicate conditions in Field + Monomial substitution function for PExpr
thery
2006-10-02
bug dans field_simplify
barras
2006-09-29
args implicites dans Field
barras
2006-09-28
separation de RealField
barras