index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
setoid_ring
Age
Commit message (
Expand
)
Author
2007-06-07
Extension of NArith: Nminus, Nmin, etc
letouzey
2007-04-29
Orthographe en passant
herbelin
2007-02-07
doc de ring/field + option infinite -> completeness
barras
2007-02-05
changement dans ring specification du sign, division
bgregoir
2007-02-02
field: introduction de Get_goal
bgregoir
2007-02-02
ring: introduction de Get_goal
bgregoir
2007-02-02
Now 1/x * x simplifies to 1
thery
2007-01-24
changement de la fonction norm_subst
bgregoir
2007-01-23
ring : Correction du bug PR#1306
bgregoir
2006-12-15
Changement dans ring et field, beaucoup de correction d'erreurs,
bgregoir
2006-12-11
Changement dans le kernel :
bgregoir
2006-11-16
pb avec r9379 + modifs dans ring
barras
2006-11-16
suite de r9362: reconnaissance de qqs injections entre nat, N et Z
barras
2006-11-10
generalisation de ring pour faire Ring_nf
barras
2006-10-30
fixed field_simplify + changed precedence of let and fun in ltac
barras
2006-10-29
Exports manquants dans ring
barras
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-26
Déplacement des propriétés générales de BinList dans List et des tactiqu...
herbelin
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-10
make sure BinList is not made visible to files that use the tactic Ring
bertot
2006-10-05
A version of natprering that should be more efficient and removal of a bad
bertot
2006-10-05
Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom
barras
2006-10-05
Corrects the problem described in PR#1240:
bertot
2006-10-04
inefficacite de field_simplify_eq
barras
2006-10-02
bug dans field_simplify
barras
2006-09-29
args implicites dans Field
barras
2006-09-29
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9188 85f007b7-540e-04...
barras
2006-09-28
separation de RealField
barras
2006-09-28
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 85f007b7-540e-04...
barras
2006-09-26
Compilation newring
notin
2006-09-26
commit de field + renommages
barras
2006-09-26
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2006-05-30
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-02-01
protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)
barras
2006-02-01
protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)
barras
2006-01-11
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2005-12-26
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...
herbelin
2005-12-02
Changement des named_context
gregoire
2005-11-18
petites corrections + contournement bug projections
barras
2005-11-18
commited first version of new ring
barras