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
*
Oubli BinNat
herbelin
2003-11-07
*
Oubli d'un Set Implicit Arguments
herbelin
2003-11-07
*
Biblio standard sans mention de la possibilite d'etre impredicatif
herbelin
2003-11-07
*
Biblio standard sans impredicativite
herbelin
2003-11-07
*
Des oublis
herbelin
2003-11-06
*
Report des definitions sorties de fast_integer pour compatibilite
herbelin
2003-11-06
*
Notations
herbelin
2003-11-05
*
Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...
herbelin
2003-11-05
*
Preuve de l'incoherence de {A}+{~A} avec Set impredicatif
herbelin
2003-11-05
*
Redondances
herbelin
2003-11-05
*
Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...
herbelin
2003-11-05
*
Exporting ^; utilisation arg scope implicite
herbelin
2003-11-03
*
Cosmetique
herbelin
2003-11-02
*
Renforcement significatif du resultat principal
herbelin
2003-11-02
*
Rien de bien important
herbelin
2003-11-02
*
Commentaires
herbelin
2003-11-02
*
Typo
herbelin
2003-11-02
*
AC + EXT -> EM
herbelin
2003-11-02
*
Relations entre le choix (forme relationnelle) avec restriction ou non
herbelin
2003-11-02
*
Renommage bool en boolP pour eviter la qualification
herbelin
2003-11-02
*
Restauration preference Rge a Rle pour compatibilite...
herbelin
2003-11-02
*
Restauration preference Rge a Rle pour compatibilite...; petit nettoyage
herbelin
2003-11-02
*
Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...
herbelin
2003-11-01
*
Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...
herbelin
2003-11-01
*
Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...
herbelin
2003-10-30
*
Choix sous sa forme relationnelle
herbelin
2003-10-29
*
Ordre (symbolique) des Require
herbelin
2003-10-28
*
Passage de la notations de paire dans core_scope
herbelin
2003-10-28
*
Passage des notations de type dans type_scope
herbelin
2003-10-28
*
Ajout %core; MAJ niveau connecteurs logique
herbelin
2003-10-28
*
MAJ
herbelin
2003-10-28
*
Fichier offrant l'axiome du choix unique en presence de logique classique
herbelin
2003-10-28
*
Fichier offrant l'axiome du choix en presence de logique classique
herbelin
2003-10-28
*
La logique sur Type inclut celle sur Set
herbelin
2003-10-28
*
Retour en arriere sur d'autres renommages de variables
herbelin
2003-10-28
*
Retour a un nommage non standard des variables pour compatibilite; report 're...
herbelin
2003-10-27
*
Bug du commit precedent
herbelin
2003-10-27
*
Commentaires
herbelin
2003-10-23
*
Documentation/Structuration
herbelin
2003-10-22
*
Documentation/Structuration
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Redondance de dec_eq_nat
herbelin
2003-10-21
*
Type relation dans Datatypes
herbelin
2003-10-21
*
Maintenant avant Datatypes
herbelin
2003-10-21
*
ajouts
herbelin
2003-10-21
*
R passe dans Set !
herbelin
2003-10-20
*
20 est uniquement associatif a gauche
herbelin
2003-10-17
*
Des implicites plus 'naturels' pour eq_ind, identity_ind and co
herbelin
2003-10-17
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
lettac -> set
barras
2003-10-16
[next]