index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
Reals
/
Ranalysis4.v
Age
Commit message (
Expand
)
Author
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2008-03-23
Une passe sur les réels:
herbelin
2006-10-17
Mise en forme des theories
notin
2006-03-28
Nommage explicite de certains "intro" pour préserver la compatibilité
herbelin
2004-07-16
Nouvelle en-tête
herbelin
2003-11-29
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-04-12
Open Scope en Local
herbelin
2003-04-10
Remplacement Import par Open Scope en v8
herbelin
2003-04-09
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".
herbelin
2003-03-12
*** empty log message ***
barras
2003-01-16
Renommage de RealsB en Rbase
desmettr
2002-11-27
Réorganisation de la librairie des réels
desmettr
2002-07-31
MAJ pour Exp_prop
desmettr
2002-07-29
MAJ pour Rtrigo_reg
desmettr
2002-07-22
Quelques ameliorations dans Reg
desmettr
2002-07-19
Regularites de pow et des sommes finies / MAJ Reg
desmettr
2002-07-19
Resultats de regularite de Rabsolu / MAJ de Reg
desmettr
2002-07-18
Correction d'un bug dans IsCont_pt
desmettr
2002-07-18
MAJ pour Sqrt_reg
desmettr
2002-07-16
*** empty log message ***
desmettr
2002-06-21
Suppression de l'axiome d'extensionnalite
desmettr
2002-06-17
Prise en compte de exp, cosh et sinh
desmettr
2002-06-11
*** empty log message ***
desmettr
2002-06-11
Ranalysis.v
desmettr