index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
setoid_ring
Commit message (
Expand
)
Author
Age
*
Changed the definition of Nminus in BinNat.v by removing comparison.
emakarov
2007-09-20
*
Raffinement de l'algorithme d'inférence de type
herbelin
2007-09-17
*
fixed bug 1448 and 1674
barras
2007-07-24
*
fixed bug 1675: computing carrier from the relation type was not right
barras
2007-07-24
*
normalisation (by closure) was not performed under fixpoints
barras
2007-07-12
*
port de r9968: bug avec les ring calculatoires
barras
2007-07-12
*
Extension of NArith: Nminus, Nmin, etc
letouzey
2007-06-07
*
Orthographe en passant
herbelin
2007-04-29
*
doc de ring/field + option infinite -> completeness
barras
2007-02-07
*
changement dans ring specification du sign, division
bgregoir
2007-02-05
*
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-02-02
*
changement de la fonction norm_subst
bgregoir
2007-01-24
*
ring : Correction du bug PR#1306
bgregoir
2007-01-23
*
Changement dans ring et field, beaucoup de correction d'erreurs,
bgregoir
2006-12-15
*
Changement dans le kernel :
bgregoir
2006-12-11
*
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-16
*
generalisation de ring pour faire Ring_nf
barras
2006-11-10
*
fixed field_simplify + changed precedence of let and fun in ltac
barras
2006-10-30
*
Exports manquants dans ring
barras
2006-10-29
*
simplif de la partie ML de ring/field
barras
2006-10-27
*
changement des _sym par _comm dans setoid_ring
bgregoir
2006-10-27
*
Déplacement des propriétés générales de BinList dans List et des tactiqu...
herbelin
2006-10-26
*
field_simplify_eq profite de la factorisation de Laurent
barras
2006-10-17
*
changes the use of lists and notations, to avoid that the notations
bertot
2006-10-16
*
Fix name clash on left
thery
2006-10-12
*
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-10
*
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-05
*
inefficacite de field_simplify_eq
barras
2006-10-04
*
bug dans field_simplify
barras
2006-10-02
*
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-29
*
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-28
*
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-09-26
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
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-02-01
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
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-26
*
Changement des named_context
gregoire
2005-12-02
*
petites corrections + contournement bug projections
barras
2005-11-18
[next]