index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
Bug niveau
herbelin
2003-05-29
*
niveau 49 devient next
herbelin
2003-05-29
*
niveau 49 devient next
herbelin
2003-05-29
*
Ne pas mettre d'associatif a droite au niveau 3 en V7
herbelin
2003-05-29
*
'only parsing' pour le passage de trucT a truc
herbelin
2003-05-27
*
"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals
herbelin
2003-05-24
*
V8Notation
herbelin
2003-05-22
*
Ajout V8Notation
herbelin
2003-05-22
*
Concentration des notations officielles dans Init/Notations; restructuration ...
herbelin
2003-05-21
*
Notations
herbelin
2003-05-21
*
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
*
Nouveaux lemmes
herbelin
2003-05-13
*
Nouveaux lemmes (sur proposition de Nijmegen)
herbelin
2003-05-13
*
Nouveaux lemmes (sur proposition de Nijmegen)
herbelin
2003-05-13
*
ajout inverse relation bien fondee
mohring
2003-05-09
*
coqide: toolbar/autosave
monate
2003-05-07
*
Blancs
herbelin
2003-04-29
*
Notations
herbelin
2003-04-29
*
Implicit Types
herbelin
2003-04-29
*
Ajout ChoiceFacts
herbelin
2003-04-29
*
Blancs
herbelin
2003-04-29
*
En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...
herbelin
2003-04-29
*
Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot
letouzey
2003-04-28
*
Intégration DatatypesSyntax à Datatypes
herbelin
2003-04-17
*
Divers
herbelin
2003-04-17
*
<> maintenant standard
herbelin
2003-04-17
*
Intégration DatatypesSyntax à Datatypes
herbelin
2003-04-17
*
Syntaxe 'x=y:>T'
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
*
Cosmetique
herbelin
2003-04-14
*
Local 'o'
herbelin
2003-04-14
*
Open Scope en Local
herbelin
2003-04-12
*
Open Scope remplace Import
herbelin
2003-04-10
*
Calcul automatique de l'implicite de nil pour que l'affichage sache le traiter
herbelin
2003-04-10
*
Remplacement Import par Open Scope en v8
herbelin
2003-04-10
*
cast de nil
herbelin
2003-04-09
*
nil en implicite dans la v8
herbelin
2003-04-09
*
Ajout Open Scope
herbelin
2003-04-09
*
Activation des implicites pour la v8
herbelin
2003-04-09
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
herbelin
2003-04-09
*
Renommage K; equivalence JMeq et eq_dep sur Type
herbelin
2003-04-09
*
Defined
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
[next]