index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Reals
Commit message (
Expand
)
Author
Age
*
Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...
herbelin
2003-09-23
*
Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...
herbelin
2003-09-21
*
Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...
herbelin
2003-09-19
*
Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...
herbelin
2003-09-19
*
Ajout et MAJ commandes de scopes
herbelin
2003-09-12
*
Bind et Delimit pour R
herbelin
2003-09-12
*
Bind et Delimit pour R
herbelin
2003-09-12
*
INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...
herbelin
2003-06-12
*
niveau 49 devient next
herbelin
2003-05-29
*
"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals
herbelin
2003-05-24
*
Bug
herbelin
2003-05-21
*
Amelioration presentation
herbelin
2003-05-14
*
Amelioration affichage
herbelin
2003-05-14
*
Suppression de 'R' dans la notation == entre
herbelin
2003-05-14
*
Suppression de 'R' dans la notation == entre
herbelin
2003-05-14
*
Deplacement lemmes sur fact de Reals vers Arith
herbelin
2003-05-14
*
En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...
herbelin
2003-04-29
*
Divers
herbelin
2003-04-17
*
<> maintenant standard
herbelin
2003-04-17
*
suite au commit d'hugo dans TypeSyntax & Raxiom, Intro donnait un nom different
letouzey
2003-04-16
*
sumboolT, sumorT, sigTT, SigT redondants
herbelin
2003-04-16
*
Local 'o'
herbelin
2003-04-14
*
Open Scope en Local
herbelin
2003-04-12
*
Remplacement Import par Open Scope en v8
herbelin
2003-04-10
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
herbelin
2003-04-09
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".
herbelin
2003-04-09
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
herbelin
2003-04-09
*
Nommage explicite des hypotheses introduites quand le nom existe aussi comme ...
herbelin
2003-04-07
*
Espaces superflus
herbelin
2003-04-07
*
Ajout Implicit Variable Type
herbelin
2003-03-31
*
*** empty log message ***
barras
2003-03-21
*
*** empty log message ***
barras
2003-03-12
*
Restructuration des hints pour qu'Auto fasse moins de détours et les
herbelin
2003-02-27
*
Ajout du theoreme de Cesaro
desmettr
2003-02-14
*
MAJ pour Reg
desmettr
2003-01-28
*
Documentation du contenu de REALS
desmettr
2003-01-22
*
Modifications dans SeqProp
desmettr
2003-01-22
*
Renommages dans Rtrigo_def
desmettr
2003-01-22
*
Commentaires
desmettr
2003-01-22
*
Renommages nombreux
desmettr
2003-01-22
*
Commentaires
desmettr
2003-01-22
*
Renommage f_pos -> IVT (Intermediate Value Theorem
desmettr
2003-01-22
*
Suppression d'un Import R_scope probablement oublie
desmettr
2003-01-22
*
Commentaires
desmettr
2003-01-22
*
Renommages dans RList
desmettr
2003-01-22
*
MAJ pour renommage Rcomplet
desmettr
2003-01-22
*
Renommages dans Rcomplete
desmettr
2003-01-22
*
Renommage Rcomplet.v -> Rcomplete.v
desmettr
2003-01-22
*
Suppression de lemmes superflus
desmettr
2003-01-22
*
Commentaires
desmettr
2003-01-22
[next]